Re: Variable pitch mode line

[Eli Zaretskii]

> Date: Fri, 24 Dec 2021 13:42:33 +0200
> From: Eli Zaretskii <eliz@gnu.org>
> Cc: larsi@gnus.org, emacs-devel@gnu.org, monnier@iro.umontreal.ca, 
> tsdh@gnu.org
> 
> > 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.

And, once again, this should be coordinated with the Texinfo folks.
We should not invent our own rules, because we don't have enough
knowledge, background, and even authority to do so.  This isn't our
territory.