Matthew Flatt 4a782c4000 fix editor refresh problem when line numbers are shown ... More generally, fix horizontal refresh when an editor has left padding. Otherwise, deleting a character in DrRacket with line numbers shown seems sluggish, because the update waits for a refresh event. original commit: 506aa79d14f2b32cc1028b0e9a8cee5b3ee0a24d		2011-10-28 20:01:19 -06:00
collects	fix editor refresh problem when line numbers are shown	2011-10-28 20:01:19 -06:00
doc/release-notes	remove unsupported MDI styles and method	2011-08-04 08:02:54 -06:00
man/man1	minor man-page corrections	2011-02-01 08:01:17 -07:00