# HG changeset patch # User wenzelm # Date 850823553 -3600 # Node ID 747177b6767001c2564156f85e3ebbc741702cc6 # Parent 853732a26bdd88fb367707bfed795bd16463b5ba fixed ML_HOME; chmod fix; diff -r 853732a26bdd -r 747177b67670 lib/scripts/run-smlnj --- a/lib/scripts/run-smlnj Tue Dec 17 12:51:54 1996 +0100 +++ b/lib/scripts/run-smlnj Tue Dec 17 12:52:33 1996 +0100 @@ -43,7 +43,7 @@ cp "$INFILE" "$OUTFILE" || fail_out fi -[ -n "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out } +[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out } MLTEXT="$EXIT $COMMIT $MLTEXT" MLEXIT="commit();" @@ -51,7 +51,7 @@ ## run it! -START_SML="$ML_HOME/bin/sml $ML_OPTIONS $DB" +START_SML="$ML_HOME/sml $ML_OPTIONS $DB" if [ -n "$TERMINATE" ]; then { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML