5 Sep
2012
5 Sep
'12
3:14 p.m.
On Sep 5, 2012, at 6:50 AM, Dennis Vennink wrote:
I'm all for it. I think a minimum size option would be better though. This way the size still fits the height of the line number font at larger sizes.
Thanks for the speedy reply (and for your work on this; my gutter now looks great!). Yes, of course, a minimum size option would make more sense.
-- Phil