> There's another bug in the manual:
>
> ------------------------------------------------------------------------
> Use the '@minus{}' command to generate a minus sign. In a fixed-width
> font, this is a single hyphen, but in a proportional font, the symbol is
> the customary length for a minus sign--a little longer than a hyphen,
> shorter than an em-dash:
>
> '-' is a minus sign generated with '@minus{}',
> ------------------------------------------------------------------------
>
> (where '-' is the ASCII hyphen-minus), which is incorrect: in the
> MPFR manual, I get the real minus sign '−'. I suspect that the
> difference is due to the chosen encoding. But the manual is silent
> on this point.
It's not incorrect, just making accommodations for the character
encoding.
FWIW, the Info file currently outputs with
‘−’ is a minus sign generated with ‘@minus{}’,
The − there is not an ASCII character. Note also the directional
quote marks.
It's possible you have an old version of the manual, or that you
are running Info in a non-UTF-8 locale where fallback characters are
used.