--- a/Admin/MacOS/App1/script Tue Jan 18 21:29:56 2011 +0100
+++ b/Admin/MacOS/App1/script Tue Jan 18 21:33:07 2011 +0100
@@ -58,6 +58,7 @@
OUTPUT="/tmp/isabelle$$.out"
+# ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
RC=$?