src/Tools/jEdit/src/jedit_options.scala
changeset 62227 6eeaaefcea56
parent 61742 fd3b214b0979
child 65236 4fa82bbb394e
--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Jan 20 23:19:52 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Thu Jan 21 20:50:34 2016 +0100
@@ -96,7 +96,7 @@
             val title = opt_title
             def load = text = value.check_name(opt_name).value
             def save =
-              try { update(value + (opt_name, text)) }
+              try { store(value + (opt_name, text)) }
               catch {
                 case ERROR(msg) =>
                   GUI.error_dialog(this.peer, "Failed to update options",