# HG changeset patch
# User wenzelm
# Date 1472744924 -7200
# Node ID 20ef5c1291da017790341c029eb0de943a4385df
# Parent  6b6bf5c0f9c1c6cefe80f70c74eefb6c7aa46183# Parent  a9159d30070fd1d81f0bd5385ff15bfa7e99aeed
merged

diff -r 6b6bf5c0f9c1 -r 20ef5c1291da src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Sep 01 17:44:21 2016 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Thu Sep 01 17:48:44 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