# HG changeset patch
# User wenzelm
# Date 1430946661 -7200
# Node ID 652a8e72cb75c9b4dd0dbe1a8551fa7ad24e43c8
# Parent  6a27919a98f00cfc71553442fd0a89866b0bdda8
less confusing default;

diff -r 6a27919a98f0 -r 652a8e72cb75 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed May 06 23:04:36 2015 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Wed May 06 23:11:01 2015 +0200
@@ -256,6 +256,7 @@
 sidekick.complete-instant.toggle=false
 sidekick.complete-popup.accept-characters=\\t
 sidekick.complete-popup.insert-characters=
+sidekick.persistentFilter=true
 sidekick.showFilter=true
 sidekick.splitter.location=721
 systrayicon=false