# HG changeset patch
# User wenzelm
# Date 1458334826 -3600
# Node ID 2f816b80e3f48ad9a2bf134df77c8ef616dd3a7e
# Parent  6cfa0de8bb993845be555bfbc18c970afc96bc40
avoid redundant addLeftOfScrollBar;

diff -r 6cfa0de8bb99 -r 2f816b80e3f4 src/Tools/jEdit/src/jEdit.props
--- 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