lib/scripts/run-smlnj-0.93
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