# HG changeset patch
# User wenzelm
# Date 1347441284 -7200
# Node ID 5eff42e69edb76a72c97aaecb062c9f4243a4da4
# Parent  a1b0654e7c90cbf5e8d6afaaecabab00e1a17e3e
tuned error;

diff -r a1b0654e7c90 -r 5eff42e69edb src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Wed Sep 12 10:18:31 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Wed Sep 12 11:14:44 2012 +0200
@@ -68,7 +68,13 @@
             name = opt_name
             val title = opt_title
             def load = text = value.check_name(opt_name).value
-            def save = update(value + (opt_name, text))
+            def save =
+              try { update(value + (opt_name, text)) }
+              catch {
+                case ERROR(msg) =>
+                  Library.error_dialog(this.peer, "Failed to update options",
+                    Library.scrollable_text(msg))
+              }
           }
         text_area.peer.setInputVerifier(new InputVerifier {
           def verify(jcomponent: JComponent): Boolean =