Hi Simon, I'm not entirely sure offhand what's happening, but as for:
Ideas on how to solve this?
1) Does texi2html do the right thing?
2) Post-process the output with a script. (I do this in other cases for
various manuals.)
Either of those will be a more practical fix than worrying about
makeinfo.
Thanks,
Karl
