author | wenzelm |
Tue, 23 Jun 2009 21:14:54 +0200 | |
changeset 34613 | 71fb6ab6ec57 |
parent 34612 | 5a03dc7a19e1 |
child 34614 | 25b178e4faaf |
src/Tools/jEdit/dist-template/properties/jedit.props | file | annotate | diff | comparison | revisions |
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Tue Jun 23 20:49:56 2009 +0200 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Tue Jun 23 21:14:54 2009 +0200 @@ -25,6 +25,7 @@ view.showToolbar=false buffer.sidekick.keystroke-parse=true sidekick.buffer-save-parse=true +sidekick.complete-delay=300 mode.isabelle.sidekick.showStatusWindow.label=true sidekick-tree.dock-position=right isabelle-state.dock-position=bottom