# HG changeset patch
# User wenzelm
# Date 1165761033 -3600
# Node ID ccb2346ee4167c681de2ecda67de9f6c424c0a81
# Parent  0c65e072f4beb8f6e7cf33e030fc9a0c33c6f7de
hardwired option -q;

diff -r 0c65e072f4be -r ccb2346ee416 lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0	Sun Dec 10 15:30:31 2006 +0100
+++ b/lib/scripts/run-polyml-5.0	Sun Dec 10 15:30:33 2006 +0100
@@ -80,10 +80,10 @@
 
 if [ "$PRG" = "$POLY" ]; then
   "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$PRG" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+    { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 else
   "$ISABELLE_HOME/lib/scripts/feeder" -p -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$PRG" $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+    { read FPID; "$PRG" -q $ML_OPTIONS "$MLTEXT"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 fi
 RC="$?"