Re: Questions about history of man/texinfo.texi