diff -r 813d8bc3192f -r fa9dfbfc4145 GUI/UserOption.cs
--- a/GUI/UserOption.cs	Sun Aug 08 13:57:26 2010 +0000
+++ b/GUI/UserOption.cs	Thu Aug 12 20:53:27 2010 +0000
@@ -54,7 +54,7 @@
       this.settings = settings;
       this.name = name;
       if (name != null)
-        this.value = settings.Get(name, value);
+        this.value = settings.GetValue(name, value);
       else
         this.value = value;
       this.menuItem = menuItem;
@@ -72,7 +72,7 @@
         if (this.value != value) {
           this.value = value;
           if (this.name != null)
-            settings.Set(name, value);
+            settings.SetValue(name, value);
           this.menuItem.Checked = value;
           if (changed != null)
             changed(this, null);