| changeset 60267 | d496ab7e0136 |
| parent 58785 | e7d2b46520e0 |
| child 60269 | 652a8e72cb75 |
--- a/src/Tools/jEdit/src/jEdit.props Wed May 06 14:23:22 2015 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Wed May 06 22:48:41 2015 +0200 @@ -256,6 +256,7 @@ sidekick.complete-instant.toggle=false sidekick.complete-popup.accept-characters=\\t sidekick.complete-popup.insert-characters= +sidekick.showFilter=true sidekick.splitter.location=721 systrayicon=false tip.show=false