tuned message;
authorwenzelm
Thu, 01 Sep 2016 17:35:01 +0200
changeset 63753 c57db6b2befc
parent 63752 79f11158dcc4
child 63754 23b013b6b2fb
tuned message;
src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 16:13:46 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 17:35:01 2016 +0200
@@ -246,11 +246,11 @@
         GUI.confirm_dialog(view,
           "Pending Isabelle/jEdit keymap changes",
           JOptionPane.OK_CANCEL_OPTION,
-          "The following Isabelle keymap changes are in conflict with",
-          "the current jEdit keymap " + quote(keymap_name) + ".",
+          "The following Isabelle keymap changes are in conflict with the current",
+          "jEdit keymap " + quote(keymap_name) + ".",
           new Table(table_model),
           "Selected shortcuts will be applied, unselected changes will be ignored.",
-          "Results are made persistent in $JEDIT_SETTINGS/properties.") == 0)
+          "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0)
     { table_model.apply(keymap_name, keymap) }
 
     no_shortcut_conflicts.foreach(_.set(keymap))