src/Tools/jEdit/src/keymap_merge.scala
changeset 67648 f6e351043014
parent 66923 914935f8a462
child 71162 4b3e1b859a22
--- 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()
   }
 }