> 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