ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
authorwenzelm
Sat Sep 17 16:00:54 2011 +0200 (2011-09-17)
changeset 44948b455e4f42c04
parent 44947 8ae418dfe561
child 44949 b49d7f1066c8
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
Admin/MacOS/App1/script
     1.1 --- a/Admin/MacOS/App1/script	Sat Sep 17 15:08:55 2011 +0200
     1.2 +++ b/Admin/MacOS/App1/script	Sat Sep 17 16:00:54 2011 +0200
     1.3 @@ -104,7 +104,8 @@
     1.4    ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
     1.5    RC=$?
     1.6  else
     1.7 -  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
     1.8 +  rm -f "$OUTPUT" && touch "$OUTPUT"
     1.9 +  "$ISABELLE_TOOL" jedit "$@"
    1.10    RC=$?
    1.11  fi
    1.12