Re: @math{-} does not produce a minus sign in Info

[Gavin Smith]

On Tue, Oct 25, 2022 at 03:28:33PM +0200, Vincent Lefevre wrote:
> With some fonts, such as DejaVu Sans Mono, the ASCII - is a very narrow
> dash (e.g. 2×4 pixels), which is fine when used as an hyphen, but looks
> too much like a dot in math expressions. With this font, the minus sign
> is larger (2×8 pixels), thus easier to read in math expressions.

Not much can be expected in terms of typographical quality for Info
output, so I don't see this as a problem for Info.

For HTML output, you have the option of using @minus{} instead, or
@math{-} with any of the HTML_MATH settings.

> Another reason is to avoid false positives when searching for a minus
> sign.

It seems like the opposite would be the case that people will be unable
to find the minus sign when searching the document because they are
unable to type it in on their keyboards.