author | wenzelm |
Sat, 17 Sep 2011 16:00:54 +0200 | |
changeset 44948 | b455e4f42c04 |
parent 44947 | 8ae418dfe561 |
child 44949 | b49d7f1066c8 |
--- 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