bug#48365: 13.0.11; Dollars in distinct comments trigger math mode highlighting in text in-between

[Tassilo Horn]

Hi Jean-Francois,

> git bisect indicates first bad commit is
>
> commit 6654955216a42936b87f76dc346aad829b1d52fb
> Date:   Wed Jun 3 01:44:32 2020 +0900
>
>     Use search-based fontification for $...$ (bug#33139)
>
> Reading the commit message, I see there was extensive discussion and
> the change seems to have been discussed in depth and well-motivated. I
> wonder if you can confirm that you see the same at your locale as me.

Yes, I see the problem.  I've pushed a fix which ignores $ in comments
just as it already ignored $ in verbatim contexts.

Could you please test and report back?

Bye,
Tassilo