Re: The defaults for Info

> Date: Thu, 1 Oct 2015 21:14:17 GMT > From: Karl Berry > > I find the File: and Node: parts of the hdr line the most useful. > At least Node:, for sure, much more than the pointers. Go figure ... Actually, the "File:" and "Node:" parts are redundant: they also appear in

Re: [bug #46083] DeclareUnicodeCharacter breaks if used twice for same character

On 03.10.2015 00:12, Karl Berry wrote: > \DeclareUnicodeCharacter{00A0}{\ } > > FWIW, A0 is supposed to be a no-break space. That's \tie, not "\ ". > > \DeclareUnicodeCharacter{03C0}{$\pi$} > > Can you please send me your list of added characters? I know well that > many math

Re: The defaults for Info

Actually, the "File:" and "Node:" parts are redundant: they also appear in the mode line. I am well aware of that (obviously). However, even though it is redundant, the the top of the screen and the bottom of the screen are two different things. I find having the basic info useful in