# 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() } }