I noticed that the @dots{} command in Texinfo produces in HTML:
      <small class="dots">...</small>

    I think it should produce:
      &hellip;

Agreed.  Patrice, unless you see a problem with it, can you do this for
texi2html (if it doesn't already).

Thanks,
k


Reply via email to