4 maj 2023 kl. 22.57 skrev Shynur Xie <one.last.kiss@outlook.com>:

I finally chose the new face that you defined, because
"highlight" is difficult to distinguish against my dark background.

Maybe we should make the `highlight` face better at highlighting then?

On white background it seems to do alright. Comparison, using `highlight`:

It indeed seems that `highlight` on dark background is a bit too timid. What about, say, #006090 instead of darkolivegreen?