Horizontal ellipsis in HTML

[Noah Slater]

Hello,

I noticed that the @dots{} command in Texinfo produces in HTML:

  <small class="dots">...</small>

I think it should produce:

  &hellip;

This produces the proper Unicode horizontal ellipsis character and has been
included in HTML since 4.0, released in 1997. I don't think we have to be
worrying about this being supported, it even works in my text mode browser.

Thanks,

-- 
Noah Slater, http://tumbolia.org/nslater