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",