# HG changeset patch
# User wenzelm
# Date 1472734624 -7200
# Node ID 962707e50fc043aa75459f6a62c64958af33dec9
# Parent  dde79b7faddf8058c495f4cf5a535941cc244888
tuned message;

diff -r dde79b7faddf -r 962707e50fc0 src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 14:49:36 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 14:57:04 2016 +0200
@@ -250,10 +250,10 @@
         GUI.confirm_dialog(jEdit.getActiveView,
           "Pending Isabelle/jEdit keymap changes",
           JOptionPane.OK_CANCEL_OPTION,
-          "The following Isabelle keymap shortcuts are in conflict with",
+          "The following Isabelle keymap changes are in conflict with",
           "the current jEdit keymap " + quote(keymap_name) + ".",
           new Table(table_model),
-          "Selected changes will be applied, unselected changes will be ignored.") == 0)
+          "Selected shortcuts will be applied, unselected changes will be ignored.") == 0)
     {
       table_model.apply(keymap_name, keymap)
       save = true