lib/scripts/run-mosml
changeset 9794 2be239143d42
parent 9789 7e5e6c47c0b5
child 9977 32955afeb835
equal deleted inserted replaced
9793:2c3d4e03e00c 9794:2be239143d42
    50 else
    50 else
    51   FEEDER_OPTS="-q"
    51   FEEDER_OPTS="-q"
    52 fi
    52 fi
    53 
    53 
    54 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    54 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    55   { read FPID; "$ML_HOME/$MOSML" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    55   { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    56 RC="$?"
    56 RC="$?"
    57 
    57 
    58 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    58 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    59 
    59 
    60 exit "$RC"
    60 exit "$RC"