# HG changeset patch
# User wenzelm
# Date 854039772 -3600
# Node ID fe15e3fcccf063ba75e6fcd97ba21cc6a730e211
# Parent  8d8344bcf98a1aa5488adf183aa5ddf5a057cf3a
'rm -f' instead of 'mv -f';

diff -r 8d8344bcf98a -r fe15e3fcccf0 lib/scripts/run-smlnj-0.93
--- 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