--- a/lib/scripts/run-mlworks Tue Sep 05 18:53:42 2000 +0200
+++ b/lib/scripts/run-mlworks Tue Sep 05 18:59:22 2000 +0200
@@ -26,7 +26,7 @@
MLWORKS="mlworks-basis -tty"
else
EXIT=""
- MLWORKS="mlimage -load \"$INFILE\" -tty"
+ MLWORKS="mlimage -load $INFILE -tty"
fi
if [ -z "$OUTFILE" ]; then
@@ -49,7 +49,7 @@
fi
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$ML_HOME/$MLWORKS" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+ { read FPID; "$ML_HOME"/$MLWORKS $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
RC="$?"
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"