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