22 Sep
2008
22 Sep
'08
6:04 p.m.
I've been assuming all along that everyone sees this problem, but then I don't think anyone has ever mentioned it, so I wonder whether it only shows up on my slow machine. Thus far it's always been easier for me to resize the window -- thereby causing whatever refiguring is necessary -- than to dig through TextDisplay to find out what goes wrong when line numbers are turned on.