# HG changeset patch
# User wenzelm
# Date 1224619211 -7200
# Node ID 4b7609ffdcd12e259baf9adccf4be5ce6fa04510
# Parent  68e172602b867196db8261c9f159ad4bb49cccbd
disabled tracing;

diff -r 68e172602b86 -r 4b7609ffdcd1 src/Tools/jEdit/dist-template/interface
--- a/src/Tools/jEdit/dist-template/interface	Tue Oct 21 21:48:44 2008 +0200
+++ b/src/Tools/jEdit/dist-template/interface	Tue Oct 21 22:00:11 2008 +0200
@@ -2,8 +2,6 @@
 #
 # Isabelle/jEdit interface wrapper
 
-set -x
-
 ## diagnostics
 
 usage()