Hi Anselm,
I'm sending this in the hope that you can apply it when you get back from your break but
before 1.8 is released. The highlighting really ought to scale in with the font size (for those of us using larger fonts). The choice of
round_nearest(h/4) works for me.
cheers, dave tweed
This archive was generated by hypermail 2.2.0 : Sun Jul 13 2008 - 14:31:44 UTC