[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: with HTML output, @minus{} is converted to a hyphen instead of a rea
From: |
Werner LEMBERG |
Subject: |
Re: with HTML output, @minus{} is converted to a hyphen instead of a real minus character |
Date: |
Wed, 12 Oct 2022 06:37:27 +0000 (UTC) |
> 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
Re: with HTML output, @minus{} is converted to a hyphen instead of a real minus character, Patrice Dumas, 2022/10/12