changeset 58746 | 68c2cbe2fd3a |
parent 57627 | 65fc7ae1bf66 |
child 58779 | aeba9ae93dd8 |
--- a/src/Tools/jEdit/src/jEdit.props Tue Oct 21 11:13:16 2014 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Tue Oct 21 13:21:59 2014 +0200 @@ -180,6 +180,7 @@ fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII firstTime=false focus-buffer-switcher.shortcut2=A+CIRCUMFLEX +foldPainter=Circle home.shortcut= insert-newline-indent.shortcut= insert-newline.shortcut=ENTER