# 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