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

Tom Tromey
2013-10-24T13:50:49Z

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.
If there's an outcry against it, it's no trouble, I can stop it any time.
Meanwhile this puts us in a position to switch over tonight or tomorrow.

Tom