> With Texinfo 6.8 and HTML output, @minus{} is converted to a hyphen > instead of a real minus character (U+2212 MINUS SIGN).
I think this is the right action for HTML. The main reason, AFAICS, is to have working copy and paste. In most cases, stuff like '-1' must be input with a normal hyphen and not with a real minus character. In other words, for all output devices that are used for cut and paste, and which don't provide a means to control the characters returned by the cut-and-paste action (as PDF can do), it makes sense to display the (inferior) input characters by default. Werner