# HG changeset patch # User wenzelm # Date 1472721948 -7200 # Node ID 1e676fcd7ede28a8e08ec5b2cd0bb3be7a3addf0 # Parent 10c08a4d39dd7b7752f3b8a80284110cdbb1b0e7 clarified; diff -r 10c08a4d39dd -r 1e676fcd7ede src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala Thu Sep 01 11:21:27 2016 +0200 +++ b/src/Tools/jEdit/src/keymap_merge.scala Thu Sep 01 11:25:48 2016 +0200 @@ -113,7 +113,7 @@ val conflicts = keymap_shortcuts.filter(s1 => s.property == s1.property && s.binding != s1.binding || - s.property != s1.property && s.binding == s1.binding) + s.property != s1.property && s.binding == s1.binding && s1.binding != "") (s, conflicts) } }