Re: Variable pitch mode line

[Juri Linkov]

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

>> Then it's the task of the Info reader to handle links between
>> manuals in the HTML format the same way as links in the Info format
>> are handled by the Info reader.
>
> 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.