Hi Vincent,
@var{b} to precision @var{prec}, a useful trick is the following:
@verbatim
...It might work reliably if you have a blank line before the @verbatim. I realize that's not exactly what you want, but for workaround purposes. Going forward, we are going to replace makeinfo with texi2html (for all output formats, despite the name, in both cases :). Patrice, does texi2html handle this correctly? Thanks for the report. karl
