Re: Variable pitch mode line

[Juri Linkov]

>> 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 main difference is in the file /usr/share/info/dir
that maintains a list of all installed manuals.

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

Even if we will support HTML in the Emacs Info reader,
distro maintainers won't be interested to include HTML files
until the standalone Info reader will be able to read HTML files.