tuned message;
authorwenzelm
Thu, 01 Sep 2016 18:16:14 +0200
changeset 63759 f81e5f492cf9
parent 63758 20ef5c1291da
child 63760 b1088b1e3b7e
tuned message;
src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 17:48:44 2016 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Thu Sep 01 18:16:14 2016 +0200
@@ -247,7 +247,7 @@
           "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) + ".",
+          "jEdit keymap " + quote(keymap_name) + ":",
           new Table(table_model),
           "Selected shortcuts will be applied, unselected changes will be ignored.",
           "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0)