Hello folks, Should I go ahead and update texinfo.tex in the doc tree to the latest version from GNU texinfo? (RT #3879, which I just created; it was a side mention in another ticket.) I've tested generation and everything works fine with the current version in the source tree. -- Russ Allbery (rra at stanford.edu) <http://www.eyrie.org/~eagle/>