Admin/MacOS/App1/script
changeset 44948 b455e4f42c04
parent 44881 ca2f585d1ebe
child 44985 272e8e4e4fc7
--- 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