src/Tools/jEdit/src/jEdit.props
changeset 60269 652a8e72cb75
parent 60267 d496ab7e0136
child 60749 f727b99faaf7
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Wed May 06 23:04:36 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Wed May 06 23:11:01 2015 +0200
     1.3 @@ -256,6 +256,7 @@
     1.4  sidekick.complete-instant.toggle=false
     1.5  sidekick.complete-popup.accept-characters=\\t
     1.6  sidekick.complete-popup.insert-characters=
     1.7 +sidekick.persistentFilter=true
     1.8  sidekick.showFilter=true
     1.9  sidekick.splitter.location=721
    1.10  systrayicon=false