src/Tools/jEdit/src/jEdit.props
changeset 60267 d496ab7e0136
parent 58785 e7d2b46520e0
child 60269 652a8e72cb75
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Wed May 06 14:23:22 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Wed May 06 22:48:41 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.showFilter=true
     1.8  sidekick.splitter.location=721
     1.9  systrayicon=false
    1.10  tip.show=false