# HG changeset patch
# User wenzelm
# Date 1438784560 -7200
# Node ID f7f2bc0e4293d7cf937861661ca6c28e068d6b75
# Parent  9980f3bcdea2be5978a8b33d429ba0779d58a4f2
proper initialization;

diff -r 9980f3bcdea2 -r f7f2bc0e4293 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Aug 05 16:13:42 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Aug 05 16:22:40 2015 +0200
@@ -36,7 +36,6 @@
     reactions += { case ButtonClicked(_) => update(selected) }
 
     def stored: Boolean = PIDE.options.bool(name)
-    def load() { selected = stored }
     def update(b: Boolean): Unit =
       GUI_Thread.require {
         if (selected != b) selected = b
@@ -45,6 +44,8 @@
           PIDE.session.update_options(PIDE.options.value)
         }
       }
+    def load() { selected = stored }
+    load()
   }
 }