# 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