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

[Vincent Lefevre]

On 2022-10-12 11:09:47 +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 should depend on --enable-encoding and USE_NUMERIC_ENTITY.  In the
> upcoming release, if --enable-encoding is not set, entities or ASCII are
> used if possible.  For minus, an ASCII minus sign is output in HTML in
> the default case.  If --enable-encoding is not set and
> USE_NUMERIC_ENTITY is set, a numeric entity representing U+2212 should
> be used.  If --enable-encoding is set the encoded character
> corresponding to U+2212 should be output.

Well, HTML supports the "minus;" character reference:
  
https://html.spec.whatwg.org/multipage/named-characters.html#named-character-references

So, even if neither --enable-encoding nor USE_NUMERIC_ENTITY is set,
"−" could be generated, just like one currently gets:

<p>The main developers of MPFR are Guillaume Hanrot, Vincent Lef&egrave;vre,
Patrick P&eacute;lissier, Philippe Th&eacute;veny and Paul Zimmermann.
</p>

Actually I can see that a real minus character is generated with the
--enable-encoding option:

  makeinfo --html --no-split --enable-encoding mpfr.texi

So, without --enable-encoding, I would suggest the use of "&minus;"
for consistency.

BTW, I thought that --enable-encoding was the default. But after,
testing, it isn't. The makeinfo(1) man page should be clarified.
Instead of

       --disable-encoding
              do not output accented and special characters in Info output
              based on @documentencoding.

       --enable-encoding
              override --disable-encoding (default).

which looks like "(default)" applies to "override --disable-encoding"
rather than just "--disable-encoding", it should say

       --disable-encoding
              do not output accented and special characters in Info output
              based on @documentencoding (default).

       --enable-encoding
              override --disable-encoding.

Or perhaps --enable-encoding should be changed to be the default:
nowadays UTF-8 is commonly used.

-- 
Vincent Lefèvre <vincent@vinc17.net> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)