[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:00:14 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/29.0.50 (x86_64-pc-linux-gnu) |
>>> 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.
>
> Perhaps, or perhaps they'll want to have Info pages that look prettier.
I don't believe that distro packagers might want to include Info manuals
in the HTML format when only Emacs will display them but not the standalone
Info reader.
>>> 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.
>
> I don't follow the logic. You can make a mode that covers as many
> files as you wish.
I meant this is not like the Emacs Info reader works.
It's not enough to enable Info-mode after visiting
an Info file. At least, you need to use Info-on-current-buffer.
And still it works only on the first Info file in the sequence
of multiple Info files.
- Re: Variable pitch mode line, (continued)
- 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, 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, 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
- Re: HTML info, Po Lu, 2021/12/24
- RE: [External] : Re: HTML info, Drew Adams, 2021/12/24