On Tue, Nov 3, 2015 at 4:46 PM, Brian Adkins <lojicdot...@gmail.com> wrote: > Maybe "Revert All to Defaults" as the button title, or a warning that it will > revert every single value in preferences?
Yeah, that's a good idea. I've pushed a change to the text in the button. Thanks! Robby -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
