--- a/lib/scripts/run-smlnj Fri Apr 25 11:11:52 1997 +0200
+++ b/lib/scripts/run-smlnj Fri Apr 25 14:12:33 1997 +0200
@@ -21,7 +21,7 @@
EXIT=""
COMMIT=""
-FIXNAME=""
+SUFFIX=""
case "$ML_SYSTEM" in
smlnj-1.0[678]*)
@@ -33,7 +33,8 @@
EXIT="fun exit 0 : unit = OS.Process.exit OS.Process.success | exit _ = OS.Process.exit OS.Process.failure;"
COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
COMMIT_RO='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\\n"); false);'
- FIXNAME=true
+ eval $($ML_HOME/.arch-n-opsys)
+ SUFFIX=".$ARCH-$OPSYS"
;;
esac
@@ -47,13 +48,7 @@
EXIT=""
fi
-if [ -z "$OUTFILE" ]; then
- COMMIT="$COMMIT_RO"
-elif [ -n "$INFILE" -a ! "$INFILE" -ef "$OUTFILE" ]; then
- [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
- cp "$INFILE" "$OUTFILE" || fail_out
-fi
-
+[ -z "$OUTFILE" ] && COMMIT="$COMMIT_RO"
[ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
MLTEXT="$EXIT $COMMIT $MLTEXT"
@@ -65,7 +60,7 @@
START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
if [ -n "$TERMINATE" ]; then
- echo "$MLTEXT" "$MLEXIT" | $START_SML
+ sh -c "echo '$MLTEXT' '$MLEXIT' | $START_SML"
RC=$?
elif [ -z "$MLTEXT" ]; then
sh -c "{ $ISABELLE_HOME/lib/scripts/ucat; echo '$MLEXIT'; } | $START_SML"
@@ -76,10 +71,7 @@
fi
#fix heap file name
-if [ -n "$OUTFILE" -a -n "$FIXNAME" ]; then
- eval $($ML_HOME/.arch-n-opsys)
- SUFFIX=$ARCH-$OPSYS
- [ -f $OUTFILE.$SUFFIX ] && mv $OUTFILE.$SUFFIX $OUTFILE
-fi
+[ -n "$OUTFILE" -a -n "$SUFFIX" -a -f "$OUTFILE$SUFFIX" ] \
+ && mv "$OUTFILE$SUFFIX" "$OUTFILE"
exit $RC