| changeset 9794 | 2be239143d42 |
| parent 9789 | 7e5e6c47c0b5 |
| child 9977 | 32955afeb835 |
--- a/lib/scripts/run-mosml Fri Sep 01 19:40:57 2000 +0200 +++ b/lib/scripts/run-mosml Fri Sep 01 19:42:11 2000 +0200 @@ -52,7 +52,7 @@ fi "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ - { read FPID; "$ML_HOME/$MOSML" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } + { read FPID; "$ML_HOME"/$MOSML $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } RC="$?" [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"