author | wenzelm |
Wed, 06 May 2015 23:11:01 +0200 | |
changeset 60269 | 652a8e72cb75 |
parent 60268 | 6a27919a98f0 |
child 60270 | a147272b16f9 |
--- 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