Re: [racket-dev] adding preferences

2010-11-02 Thread Matthias Felleisen
And everybody else sees that you learned this from the __implementation__ rather than the __documentation__ :-) On Nov 2, 2010, at 1:11 AM, Jon Rafkind wrote: > nevermind, I see preferences:add-to-general-checkbox-panel in > drracket/private/main.rkt > > On 11/01/2010 10:27 PM, Jon Rafkind

Re: [racket-dev] adding preferences

2010-11-01 Thread Jon Rafkind
nevermind, I see preferences:add-to-general-checkbox-panel in drracket/private/main.rkt On 11/01/2010 10:27 PM, Jon Rafkind wrote: > I currently have a preference to enabling/disabling line numbers in the > 'view' menu which is easy to set up in drracket/collects/main.rkt. A > user asked me to add

[racket-dev] adding preferences

2010-11-01 Thread Jon Rafkind
I currently have a preference to enabling/disabling line numbers in the 'view' menu which is easy to set up in drracket/collects/main.rkt. A user asked me to add a checkbox they could select in edit->preferences->general which I see is controlled by framework/private/preferences.rkt but I can't see