That's why it's spelled out, so people don't use the Unicode visual duplicate in most fonts if some engine substitutes it, as Mantis does sometimes. Probably because '/' missing from following tag closure. In a message dated 5/26/2017 11:12:17 A.M. Eastern Daylight Time, stephane.chaze...@gmail.com writes:
> On page 2562 line 82990-82993 section cd, > change:<blockquote>−<blockquote>When a <hyphen-minus> is used as the > operand, this shall be equivalent to the command: [...] Note that that "−" above is a "minus sign" (U+2212), not a "-" "hyphen minus" (U+002D).
