# HG changeset patch
# User wenzelm
# Date 1317125860 -7200
# Node ID bf7a8906c0cb8230de2e729e551c12ac0e3d819f
# Parent  a43694a0b726252eb566c0bddd9638c9ce8bca34
retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);

diff -r a43694a0b726 -r bf7a8906c0cb Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Tue Sep 27 00:03:11 2011 +0200
+++ b/Admin/MacOS/App1/script	Tue Sep 27 14:17:40 2011 +0200
@@ -106,8 +106,7 @@
   ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
   RC=$?
 else
-  rm -f "$OUTPUT" && touch "$OUTPUT"
-  "$ISABELLE_TOOL" jedit "$@"
+  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
   RC=$?
 fi