[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Variable pitch mode line
From: |
Juri Linkov |
Subject: |
Re: Variable pitch mode line |
Date: |
Thu, 23 Dec 2021 21:39:05 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/29.0.50 (x86_64-pc-linux-gnu) |
>> 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.
- Re: Variable pitch mode line, (continued)
- Re: Variable pitch mode line, Stefan Kangas, 2021/12/22
- Re: Variable pitch mode line, Juri Linkov, 2021/12/22
- Re: Variable pitch mode line, Tassilo Horn, 2021/12/22
- Re: Variable pitch mode line, Juri Linkov, 2021/12/23
- Re: Variable pitch mode line, Stefan Kangas, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line, Juri Linkov, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line,
Juri Linkov <=
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line, Juri Linkov, 2021/12/23
- Re: Variable pitch mode line, Lars Ingebrigtsen, 2021/12/23
- Re: Variable pitch mode line, Juri Linkov, 2021/12/23
- Re: Variable pitch mode line, Lars Ingebrigtsen, 2021/12/23
- Re: Variable pitch mode line, Juri Linkov, 2021/12/23
- Re: Variable pitch mode line, Stefan Monnier, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line, Stefan Monnier, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23