diff: fix bug with install overwriting mmake

[Fergus Henderson]

Fix a bug reported by Warwick Harvey <wharvey at cs.monash.edu.au>.

scripts/Mmakefile:
	Make sure we delete the installed `mmake' file, if any,
	before (re)installing it, to avoid problems that can occur
	if we overwrite the script while it is still running.

Index: scripts/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/mercury/scripts/Mmakefile,v
retrieving revision 1.10
diff -u -r1.10 Mmakefile
--- Mmakefile	1998/10/17 06:14:25	1.10
+++ Mmakefile	1998/10/29 12:11:36
@@ -57,6 +57,9 @@
 .PHONY: install_scripts
 install_scripts: $(SCRIPTS)
 	[ -d $(INSTALL_BINDIR) ] || mkdir -p $(INSTALL_BINDIR)
+	# we remove the installed `mmake' script before (re)installing it
+	# to avoid overwriting the script while it is running
+	-rm -f $(INSTALL_BINDIR)/mmake
 	cp $(SCRIPTS) $(INSTALL_BINDIR) 
 	for file in $(SCRIPTS); do \
 		chmod u+w $(INSTALL_BINDIR)/$$file ;\

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.