# HG changeset patch
# User wenzelm
# Date 1229791980 -3600
# Node ID 1a574ef872547ff8e9ce4808c3357d870d51d0cc
# Parent  c880492754d070850ef686f36e3d95c6bfdc34bd
tuned sidekick properties;

diff -r c880492754d0 -r 1a574ef87254 src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Sat Dec 20 17:41:57 2008 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Sat Dec 20 17:53:00 2008 +0100
@@ -21,5 +21,7 @@
 view.gutter.fontsize=12
 view.middleMousePaste=true
 view.showToolbar=false
+buffer.sidekick.keystroke-parse=true
+sidekick.buffer-save-parse=true
 sidekick-tree.dock-position=right
 isabelle-state.dock-position=bottom