# HG changeset patch
# User wenzelm
# Date 1316268054 -7200
# Node ID b455e4f42c0401af086a48584c804f2cea20fa0a
# Parent  8ae418dfe5618f3571da3f690e1dad275482ed30
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;

diff -r 8ae418dfe561 -r b455e4f42c04 Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Sat Sep 17 15:08:55 2011 +0200
+++ b/Admin/MacOS/App1/script	Sat Sep 17 16:00:54 2011 +0200
@@ -104,7 +104,8 @@
   ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
   RC=$?
 else
-  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
+  rm -f "$OUTPUT" && touch "$OUTPUT"
+  "$ISABELLE_TOOL" jedit "$@"
   RC=$?
 fi