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