Re: Opinions on look of documentation

[Mike Miller]

On Fri, Dec 11, 2015 at 17:12:37 -0500, John W. Eaton wrote:
> Changing texinfo.tex won't have any effect on the output from makeinfo.  It
> will only change the PDF or DVI+PostScript output.

I'd object to modifying and maintaining a custom texinfo.tex again, it's
much better to go forward following the upstream improvements if we keep
using the one maintained in gnulib.

> Hmm, I don't see the problem on my system.  I'm using
> 
>   $ makeinfo --version
>   texi2any (GNU texinfo) 6.0

I also don't see the extra space with makeinfo 6.0. It is there with
makeinfo 4.13.

-- 
mike