# HG changeset patch
# User wenzelm
# Date 1290969052 -3600
# Node ID d71fe93e8e0c27c428eeb620944fe2472b904dd2
# Parent  cd7b17ba502b3bc96f273355ce1fba49d15c462c
less frequent sidekick parsing, which is relatively slow;

diff -r cd7b17ba502b -r d71fe93e8e0c src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Sun Nov 28 18:31:54 2010 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Sun Nov 28 19:30:52 2010 +0100
@@ -5,7 +5,7 @@
 buffer.lineSeparator=\n
 buffer.maxLineLen=100
 buffer.noTabs=true
-buffer.sidekick.keystroke-parse=true
+buffer.sidekick.keystroke-parse=false
 buffer.tabSize=2
 console.encoding=UTF-8
 console.font=IsabelleText