On Tuesday, 15 January 2013 at 13:55:53 UTC, Timon Gehr wrote:
On 01/15/2013 11:57 AM, mist wrote:
Well, probably I am playing "good vision nazi" here, as 12
font size
seems HUGE to me, far beyond the comfort zone.
It's just preference. I do not have any problems with font size
9.
I do not know of any editor that does not support "ctrl + scroll"
to change the font sizes on the fly.
I always change the font size of my editor, depending on how
concentrated I am, my position in my seat, or by how complicated
the current algorithm is. Or simply if somebody is looking over
my shoulder.
Your editor's font size should not be statically dictated by a
single number.
