Re: Variable pitch mode line

[Eli Zaretskii <eliz@gnu.org>]

> From: Juri Linkov <juri@linkov.net>
> Cc: stefankangas@gmail.com,  tsdh@gnu.org,  larsi@gnus.org,
>   emacs-devel@gnu.org
> Date: Thu, 23 Dec 2021 21:39:05 +0200
> 
> >> Why HTML files couldn't be installed in the same dir where all files
> >> in the Info format are installed?
> >
> > Because AFAIK that's not the canonical place where HTML docs are
> > installed, they are somewhere in /usr/share/doc/.
> 
> But these files are not HTML docs, they are Info docs in HTML format.

What's the difference?  They are HTML files, complete with index.html
and other stuff.  Look in your /usr/share/doc directory and tell me
what significant differences are between, say, GTK docs and the HTML
formatted manuals produced by makeinfo from Texinfo sources.

> > The additional difficulty, apart of the top-level directory, is that
> > HTML docs can either be produced as a single file or as separate files
> > per chapter/section, and then the directory structure (and
> > correspondingly the job of resolving links) becomes more complicated.
> >
> > It isn't rocket science to fix this, but it's not something distro
> > maintainers can do, it's something Texinfo should do, perhaps
> > consulting with us.
> 
> Then distro maintainers could always generate a single file.

You assume they will want to.  Browsing a short HTML file is easier
than browsing a long one: for example, accurate scrolling by the
scroll-bar is much easier.  I don't think it's a good idea to assume
the distributed HTML will always be a single file.

Anyway, we are discussing this in the wrong place.  If we want to lead
the move towards using HTML docs, we need to discuss this with Texinfo
folks, because they need to do the footwork, and they also need to be
aware of the move.