# HG changeset patch # User wenzelm # Date 1472744809 -7200 # Node ID a9159d30070fd1d81f0bd5385ff15bfa7e99aeed # Parent 23b013b6b2fb8b9f6b880ec6adde5c0fa4c1ace1 avoid conflict after initial keymap migration; diff -r 23b013b6b2fb -r a9159d30070f src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Sep 01 17:35:17 2016 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Thu Sep 01 17:46:49 2016 +0200 @@ -177,6 +177,7 @@ encodingDetectors=BOM XML-PI buffer-local-property end.shortcut= expand-abbrev.shortcut2=CA+SPACE +expand-folds.shortcut= fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII firstTime=false focus-buffer-switcher.shortcut2=A+CIRCUMFLEX