author | wenzelm |
Wed, 06 May 2015 22:48:41 +0200 | |
changeset 60267 | d496ab7e0136 |
parent 60266 | a2fa0e01302d |
child 60268 | 6a27919a98f0 |
--- 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