| From: Pierpaolo Bernardi (olopierpa at gmail.com) Date: Mon Mar 26 03:41:06 EDT 2012 |
|
On Sun, Mar 25, 2012 at 03:25, Robby Findler <robby at eecs.northwestern.edu> wrote: > So I've pushed a change to DrRacket that adds a preference. The > preference defaults to "no additional spacing" under windows and "one > extra pixel" (the 5.2.1 behavior) everywhere else. > > Please let me know if things start to look strange elsewhere! Thanks! Will keep open eyes. 8^) P.
| Posted on the users mailing list. |
|
![[logo]](/logo.png){kind=logo}