# HG changeset patch
# User wenzelm
# Date 1472744101 -7200
# Node ID c57db6b2befc4b9abae3ecdcf04b1c3dcf8afd68
# Parent  79f11158dcc41990fa0e85790f1e048d3289ca4f
tuned message;

diff -r 79f11158dcc4 -r c57db6b2befc 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))