Re: Variable pitch mode line

[Eli Zaretskii]

> From: Juri Linkov <juri@linkov.net>
> Date: Fri, 24 Dec 2021 10:21:59 +0200
> Cc: Lars Ingebrigtsen <larsi@gnus.org>, Tassilo Horn <tsdh@gnu.org>,
>  emacs-devel@gnu.org
> 
> Currently HTML files are generated in the source dir, that is wrong:
> 
>   doc/emacs/emacs.html
> 
> The correct place would be in the Info output dir:
> 
>   info/emacs.html

No, it should have its own subdirectory, probably html/.  Mixing Info
and HTML files is asking for trouble, particularly for "make install".

> so it could reuse INFOPATH to find HTML Info manuals as well.

No, INFOPATH should be reserved for Info files only.  Its rules (like
"::" at the beginning and end of the value) don't fit HTML docs.

> 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.