more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings();
authorwenzelm
Sat, 17 Feb 2018 20:03:37 +0100
changeset 67648 f6e351043014
parent 67647 27f3dceb5a70
child 67649 1e1782c1aedf
more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings();
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()
   }
 }