subject:"\[racket\] DrRacket Tools\/plugins info wanted"

Re: [racket] DrRacket Tools/plugins info wanted

2013-07-30 Thread Matthias Felleisen

I think it would also help if the doc pages cited by the OP were to list all tools coming with the main distribution and explain how to disable them a bit more. That's less work than coding. -- Matthias On Jul 29, 2013, at 1:01 PM, Robby Findler wrote: > [moved to dev@] Would it be someth

[racket] DrRacket Tools/plugins info wanted

2013-07-29 Thread Jon Kleiser

Hi, On one of my older Macs, DrRacket uses quite some time to launch, and I wondered if disabling some of the 17 Tools in the Preferences could help. Before disabling any of these, however, I'd like some info about what they really do. Looking here didn't make me any wiser: