[m-rev.] diff: repeated makebatch -d

[Zoltan Somogyi]

tools/makebatch:
	Avoid errors that can arise from repeated invocations of makebatch -d.

Zoltan.

cvs diff: Diffing .
Index: makebatch
===================================================================
RCS file: /home/mercury1/repository/mercury/tools/makebatch,v
retrieving revision 1.22
diff -u -b -r1.22 makebatch
--- makebatch	14 Apr 2002 17:29:27 -0000	1.22
+++ makebatch	23 Apr 2002 14:57:51 -0000
@@ -254,6 +254,10 @@
 
 	if $save_stage2
 	then
+		# If a directory with this name already exists,
+		# it probably came from a previous invocation of this script.
+		# This invocation supersedes earlier ones.
+		/bin/rm -fr stage2.batch.$visn > /dev/null
 		mv stage2 stage2.batch.$visn
 	fi
 
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------