I noticed that the @dots{} command in Texinfo produces in HTML:
<small class="dots">...</small>
I think it should produce:
…
Agreed. Patrice, unless you see a problem with it, can you do this for
texi2html (if it doesn't already).
Thanks,
k
