TeXinfo: 1999-03-26.17 A newer version of texinfo.tex should fix this bug without the need for your workaround.