changeset 2551 | fe15e3fcccf0 |
parent 2440 | b3ac45aba238 |
child 2622 | 80a81a36dd81 |
--- a/lib/scripts/run-smlnj-0.93 Thu Jan 23 18:14:20 1997 +0100 +++ b/lib/scripts/run-smlnj-0.93 Thu Jan 23 18:16:12 1997 +0100 @@ -58,7 +58,8 @@ fi if [ -n "$MOVE" -a -f "$OUTFILE" ]; then - mv -f "$OUTFILE" "$INFILE" || fail_out + rm -f "$INFILE" || fail_out + mv "$OUTFILE" "$INFILE" || fail_out fi exit $RC