# HG changeset patch
# User wenzelm
# Date 1518894217 -3600
# Node ID f6e351043014fe02f2df3ce3ec50578aada05f2c
# Parent  27f3dceb5a70486c65bb21d08150eb75e6334782
more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings();

diff -r 27f3dceb5a70 -r f6e351043014 src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Sat Feb 17 19:37:18 2018 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Sat Feb 17 20:03:37 2018 +0100
@@ -253,7 +253,7 @@
     no_shortcut_conflicts.foreach(_.set(keymap))
 
     keymap.save()
-    keymap_manager.reload()
     jEdit.saveSettings()
+    jEdit.propertiesChanged()
   }
 }