# HG changeset patch
# User wenzelm
# Date 855587815 -3600
# Node ID 1effe74134860bb9ac15a7bcdf9161c9aa56274e
# Parent  605e54988d50f31843d9f4efa6999e1acd9e0eab
tuned startup;
semi fix of piping-quit peoblem (should work on systems with *real& sh);

diff -r 605e54988d50 -r 1effe7413486 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Feb 10 15:45:31 1997 +0100
+++ b/lib/scripts/run-polyml	Mon Feb 10 16:16:55 1997 +0100
@@ -67,12 +67,15 @@
 if [ -n "$TERMINATE" ]; then
   echo "$MLTEXT" | $START_POLY
   RC=$?
+elif [ -z "$MLTEXT" ]; then
+  sh -c "$ISABELLE_HOME/lib/Tools/symbolinput | $START_POLY"
+  RC=$?
 else
-  { echo "$MLTEXT"; $ISABELLE_HOME/lib/Tools/symbolinput } | $START_POLY
+  sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; } | $START_POLY"
   RC=$?
 fi
 
 NEW_DB_INFO=$(ls -l "$DB")
-[ $RC -eq 0 -a -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
+[ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
 
 exit $RC