#5890

CaptainFlint
Participant

Yes, resetting fixed this. Now I remembered that I played a bit with manual comment highlighting (because of this problem, still unsolved), and my highlight rule remained from those experiments. Strange, that I did not notice it before…

Sorry for the false alarm.