clarified options;

--- 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"; }