tuned message;
authorwenzelm
Thu, 01 Sep 2016 14:57:04 +0200
changeset 63746 962707e50fc0
parent 63745 dde79b7faddf
child 63747 b9b5a0ab54ee
tuned message;
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