[racket] DrRacket Tools/plugins info wanted
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:
<http://docs.racket-lang.org/drracket/prefs-explanation.html#%28part._.Tools%29>
... except that those "tools" are also called "plugins".
I cannot see that this page <http://docs.racket-lang.org/tools/> has the
info that I'm looking for either.
/Jon