Werner,
> I see two possible solutions.
>
> . Define a new grotty (pseudo) font `CR' which is the same as all
> other fonts but contains an additional line
>
> \- 24 0 0x002D
> ...
>
> . Introduce a new escape, say, `\=', which maps to U+002D. ...
Hmm, the second solution would require many changes to existing manpages.
You observed already that command-line examples (where copy&paste is relevant)
could be restricted to a different font.
In fact, I guess such command-line examples are most often rendered in a
fixed-width font.
Furthermore, in fixed-width fonts (regardless which output device) the
MINUS SIGN U+2212 and the HYPHEN-MINUS U+002D often have the same appearance.
Whereas in proportional fonts, U+2212 is usually wider than U+002D.
So, a third, compromise solution is:
- On all output devices (utf8, html, dvi, ps) map \- to U+002D in fixed-width
fonts and to U+2212 in proportional fonts.
How does that sound?
Bruno
