[racket-dev] [plt] Push #21078: master branch updated

On Tue, Sep 14, 2010 at 9:13 AM, Eli Barzilay <eli at barzilay.org> wrote:
> Right -- this is why I suggested a simple extension: allow tools to
> change the default values.  Without that, the current situation is
> creating more implicit dependencies such as this commit.

Do you think that this is needed if my suggestion (made earlier,
namely to have "#lang" line-specific settings that can be augmented by
user's preferences) is done?

> Not too related: the reason that I need to actually change the
> preferences is that students already had the (lacking) default in
> their preferences.  One way to solve that would be to record in the
> preference only the divergence from the default -- what you added and
> what you removed -- so changing the default will propagate as needed.
> But this is a UI problem (if you click "OK" -- does that mean that you
> want the current set and nothing else?), and a better solution would
> be a "restore defaults" button.

There is a restore defaults button, but it is global.

Robby