Re: [racket-users] DrRacket prefs?

2018-05-24 Thread Stephen Foster
Wow! This is great, thanks! On Thu, May 24, 2018 at 11:47 AM Robby Findler wrote: > It may be easier to use the higher-level library, calling > preferences:set-default and preferences:set. Using that approach has > the advantage you don't need to know all of the

Re: [racket-users] DrRacket prefs?

2018-05-24 Thread Robby Findler
It may be easier to use the higher-level library, calling preferences:set-default and preferences:set. Using that approach has the advantage you don't need to know all of the prefs (that are machine config and OS specific, generally), but it has the disadvantage that you need to figure out what

Re: [racket-users] DrRacket prefs?

2018-05-24 Thread Stephen Foster
Nice! I'll try that! On Thu, May 24, 2018 at 11:34 AM Shu-Hung You < shu-hung@eecs.northwestern.edu> wrote: > Hi Stephen, > > Running (find-system-path 'pref-file) in the REPL shows the path to > the preference file. Inside the file there's one line like: > >

Re: [racket-users] DrRacket prefs?

2018-05-24 Thread Shu-Hung You
Hi Stephen, Running (find-system-path 'pref-file) in the REPL shows the path to the preference file. Inside the file there's one line like: (plt:framework-pref:framework:display-line-numbers #t) I don't know if directly copying the pref file to another computer would work but perhaps worth a

[racket-users] DrRacket prefs?

2018-05-24 Thread Stephen Foster
Hi, I know how to hide/show line numbers from within DrRacket's GUI. But is there a way to toggle this from the command line? I have a few hundred computers with DrRacket installed, and I want to make them all show line numbers by default. (I'd rather not do it by hand.) Is there a command