Updating texinfo.tex

[Sam Hartman]

>>>>> "Russ" == Russ Allbery <rra at stanford.edu> writes:

    Russ> Hello folks,
    Russ> Should I go ahead and update texinfo.tex in the doc tree to the latest
    Russ> version from GNU texinfo?  (RT #3879, which I just created; it was a side
    Russ> mention in another ticket.)  I've tested generation and everything works
    Russ> fine with the current version in the source tree.

If you're going to do it, do so now rather than later.

--Sam