<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Looking way too small to my eyes as of Version 2.0 (9300)... <div><br></div><div>These are a user interface element: They need to be clearly visible, unambiguous (as they get small, even the direction get ambiguous, they start to be interpretable as looking up to the left) they need to be a target that is hittable without conscious planning, and also good if it stays a fixed location.</div><div><br></div><div>There seemed a time about a week ago when they were looking nice, perhaps with a subtle disk behind them? (or am I making that up?)<br><div><br></div><div>For my money, I would keep them the height of the gutter line numbers: there’s a ton of space... use it.</div><div>t</div><div><br></div><div><img id="1c3eafec-edd8-4755-8e91-515702500015" height="115" width="468" apple-width="yes" apple-height="yes" src="cid:32435FEF-65E5-43B4-A925-016AFAEBA04B@ed.ac.uk"><br><div><br><div><div>On 5 Sep 2012, at 4:14 PM, Phil Schumm <<a href="mailto:pschumm@uchicago.edu">pschumm@uchicago.edu</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">On Sep 5, 2012, at 6:50 AM, Dennis Vennink wrote:<br><blockquote type="cite">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.<br></blockquote><br>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.<br></blockquote></div><br></div></div></div></body></html>