On Tue, Sep 14, 2010 at 9:13 AM, Eli Barzilay <e...@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 _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev