| changeset 62675 | 2f816b80e3f4 |
| parent 61529 | 82fc5a6231a2 |
| child 63236 | 48bc9045866e |
--- a/src/Tools/jEdit/src/jEdit.props Fri Mar 18 21:55:46 2016 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Fri Mar 18 22:00:26 2016 +0100 @@ -181,6 +181,7 @@ firstTime=false focus-buffer-switcher.shortcut2=A+CIRCUMFLEX foldPainter=Circle +gatchan.highlight.overview=false home.shortcut= insert-newline-indent.shortcut= insert-newline.shortcut=ENTER