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