retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);
authorwenzelm
Tue Sep 27 14:17:40 2011 +0200 (2011-09-27 ago)
changeset 45095bf7a8906c0cb
parent 45094 a43694a0b726
child 45096 7a1302b22a11
retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);
Admin/MacOS/App1/script
     1.1 --- a/Admin/MacOS/App1/script	Tue Sep 27 00:03:11 2011 +0200
     1.2 +++ b/Admin/MacOS/App1/script	Tue Sep 27 14:17:40 2011 +0200
     1.3 @@ -106,8 +106,7 @@
     1.4    ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
     1.5    RC=$?
     1.6  else
     1.7 -  rm -f "$OUTPUT" && touch "$OUTPUT"
     1.8 -  "$ISABELLE_TOOL" jedit "$@"
     1.9 +  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
    1.10    RC=$?
    1.11  fi
    1.12