Re: File missing from the git: texinfo/texinfo.tex

Hans-Peter Nilsson
2013-10-24T15:50:55Z

> From: Tom Tromey <tromey@redhat.com>
> Date: Thu, 24 Oct 2013 15:50:38 +0200

> Pedro> Yeah. If it were up to me, I'd just bite the bullet and do
> Pedro> this.
>
> I restarted the conversion here, with the texinfo bug fixed.

FWIW, I noticed no other issues while working around the texinfo
issue.

brgds, H-P