Re: with HTML output, @minus{} is converted to a hyphen instead of a real minus character

[Gavin Smith]

On Wed, Oct 12, 2022 at 11:11:53AM +0200, Patrice Dumas wrote:
> On Wed, Oct 12, 2022 at 01:13:07AM +0200, Vincent Lefevre wrote:
> > With Texinfo 6.8 and HTML output, @minus{} is converted to a hyphen
> > instead of a real minus character (U+2212 MINUS SIGN).
> 
> It is actually not clear to me why an ASCII - is output in the default
> case, and not −.  Maybe it was for compatibility with the US-ASCII
> default encoding?
> 
> This could be changed now the UTF-8 is the default encoding.
> 
> Opinions?

I think just output it as −, or as the numeric entity or raw
UTF-8 character depending on settings.

I guess it was not output as − because this was not an entity in
older versions of HTML, or it wasn't supported by browsers or the minus
sign didn't exist as a distinct codepoint in 8-bit encodings, but if
the user puts @minus{} in a document (which is rare), − is a fair
translation of this.

I think it is the %xml_text_entity_no_arg_commands_formatting hash in
tp/Texinfo/Convert/Converter.pm that needs to altered.