--- 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()
}
}