# HG changeset patch
# User wenzelm
# Date 1472746574 -7200
# Node ID f81e5f492cf9c20f93e3e9105eb59517fb3b6f19
# Parent  20ef5c1291da017790341c029eb0de943a4385df
tuned message;

diff -r 20ef5c1291da -r f81e5f492cf9 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)