Re: Variable pitch mode line

[Lars Ingebrigtsen]

Eli Zaretskii <eliz@gnu.org> writes:

>> Then after visiting the generated HTML with eww, when proportional fonts
>> are enabled with `eww-toggle-fonts`, the output looks nice.
>> But rendering a large HTML file takes too much time.  So while
>> a single HTML file is still preferable over multifile Info manuals,
>> the Info reader should limit rendering to the currently displayed
>> Info node only.
>
> Which probably means we should produce a separate file per node or
> chapter.

Not necessarily -- the HTML-ified info mode doesn't have to parse (and
render) the entire HTML file.  (There would have to be enough semantic
information in the HTML file to allow it to identify a node, which
shouldn't be a problem.)

-- 
(domestic pets only, the antidote for overdose, milk.)
   bloggy blog: http://lars.ingebrigtsen.no