Re: info: display '--' as '-'

2012-08-07 Thread Jeff King
On Tue, Aug 07, 2012 at 09:17:50AM +0200, David Kastrup wrote: > Not really: @display does not change fonts, merely indentation. From > the Texinfo manual: > [...] > But in non-typewriter fonts, -- is a shorthand for an en-dash (see > "conventions" in the Texinfo manual): Thanks, that's the miss

Re: info: display '--' as '-'

2012-08-07 Thread Andreas Schwab
Jeff King writes: > The data looks OK in user-manual.texi, but "--" is converted to "-" in > git.info. So either: > > 1. There is a bug in makeinfo, which should not be doing this > conversion inside a "@display" section. The texinfo manual says that @display does not change the font (unl

Re: info: display '--' as '-'

2012-08-07 Thread David Kastrup
Jeff King writes: > On Mon, Aug 06, 2012 at 11:08:39AM +0800, mofaph wrote: > >> I am using Git 1.7.11.4 now. I compile and then install it from the repo. >> >> $ git checkout v1.7.11.4 >> $ make prefix=$HOME/opt/git/1.7.11.4 all doc info >> $ make prefix=$HOME/opt/git/1.7.11.4 install{,-doc,-ht

Re: info: display '--' as '-'

2012-08-06 Thread Jeff King
On Mon, Aug 06, 2012 at 11:08:39AM +0800, mofaph wrote: > I am using Git 1.7.11.4 now. I compile and then install it from the repo. > > $ git checkout v1.7.11.4 > $ make prefix=$HOME/opt/git/1.7.11.4 all doc info > $ make prefix=$HOME/opt/git/1.7.11.4 install{,-doc,-html,-info} > > Recently, I f