author | wenzelm |
Tue, 21 Oct 2014 13:21:59 +0200 | |
changeset 58746 | 68c2cbe2fd3a |
parent 58745 | 5d452cf4bce7 |
child 58747 | c680f181b32e |
--- 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