bug#33967: [Feature Request] Use proportional fonts in Info-mode

[Alex Griffin]

On Thu, Jan 3, 2019, at 9:23 PM, Alan Mackenzie wrote:
> I'm happy to do without such "improvements", taking advantage of the high
> readability of my terminal's fixed width font.  I take it you really mean
> "have the option of using proportional fonts".  I've nothing against
> that.

Just having the option would be a nice improvement, there's no need to agree on 
the relative readability of each. Using more varied faces would also make it 
possible for you to style more elements of info manuals even in the terminal.

> I'm wholly unconvinced that making Info "better match" HTML is at all
> worthwhile.  Where's the advantage in such a match, even supposing it is
> possible?

I guess I don't care whether they match or not. I was just calling attention to 
the fact that texinfo already knows what needs to be formatted in fixed-width. 
(In contrast, most man pages don't track the semantic information that's 
necessary to render them in anything but fixed-width.)

-- 
Alex Griffin