--- 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=$?