[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 20:35:47 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/29.0.50 (x86_64-pc-linux-gnu) |
>> The only way to reliably support variable pitch in the Info reader
>> is by using HTML output from Texinfo and rendering it with eww/shr.
>>
>> But the problem is that most GNU/Linux distributions still don't include
>> Info manuals in the HTML format alongside with the Info format.
>> Thus we are stuck with monospaced Info manuals forever.
>
> Well, not necessarily. If we started making HTML the preferred format
> for the `C-h i' etc, then they'd probably follow after a while. And
> it'd be fine for some manuals to be in HTML while other remain in INFO.
Probably not before the standalone Info reader will support HTML.
> But nobody's yet to make an info-html-minor mode (or a major mode a la
> eww building upon shr), so it's still academic.
It can't be a mode because some Info manuals are split among several files.
- Re: Variable pitch mode line, (continued)
- 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, 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, Lars Ingebrigtsen, 2021/12/23
- Re: Variable pitch mode line,
Juri Linkov <=
- 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
- HTML info, Yuan Fu, 2021/12/23
- Re: HTML info, Juri Linkov, 2021/12/24
- Re: HTML info, Eli Zaretskii, 2021/12/24
- Re: HTML info, Lars Ingebrigtsen, 2021/12/24