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

[Eli Zaretskii]

> Date: Wed, 12 Oct 2022 06:37:27 +0000 (UTC)
> Cc: bug-texinfo@gnu.org
> From: Werner LEMBERG <wl@gnu.org>
> 
> 
> > 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.

FWIW, IME there's rarely a single alternative that can satisfy all the
use cases of cut/paste.  That's why applications have several
different methods of "pasting", which allow the user to select the
alternative suitable for the text into which they paste.  It is not
unthinkable to have one such paste alternative convert U+2212 to the
ASCII hyphen.

IOW, I'm not sure the needs of the pasting are of any concern for
makeinfo, or the program which produces the text for display in
general.  That should be the concern of the program which pastes and
of the user of that program.