ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
authorwenzelm
Sat, 17 Sep 2011 16:00:54 +0200
changeset 44948 b455e4f42c04
parent 44947 8ae418dfe561
child 44949 b49d7f1066c8
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
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