[Bug: xemacs-beta tip] decade-old version of texinfo.tex