Comment 3 for bug 1181678

THX for feeding the doc into Texinfo-5.1 again.
I'm still on makeinfo-4.13, so I cannot check myself yet.
Thus, the problem will remain unless someone sends us a patch.

On a medium time-scale I'm inclined to switch to plain LaTeX
and drop Texinfo. The vast majority of users doesn't read the
documentation at all. The rest prefers PDF. Or whatever HTML,
if it only is on a public server.