# HG changeset patch
# User wenzelm
# Date 1375387549 -7200
# Node ID 21843a4c6ba99c4527d92ea67e422fabfce76bb9
# Parent  980ca3d6ded401ceb8dc6d60708187ada1be2cf9
clarified options;

diff -r 980ca3d6ded4 -r 21843a4c6ba9 lib/scripts/run-polyml-5.5.1
--- a/lib/scripts/run-polyml-5.5.1	Thu Aug 01 21:56:43 2013 +0200
+++ b/lib/scripts/run-polyml-5.5.1	Thu Aug 01 22:05:49 2013 +0200
@@ -71,6 +71,7 @@
     FEEDER_OPTS=""
   else
     FEEDER_OPTS="-q"
+    ML_OPTIONS="$ML_OPTIONS --error-exit"
   fi
   "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
     { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }