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