From 777dc33ca65659208a5ed37e33ad4127ea087436 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 10 Mar 2009 10:32:31 +0000
Subject: Fix to use  in place of make, see
 http://proofgeneral.inf.ed.ac.uk/trac/ticket/262

---
 Makefile       | 8 ++++----
 Makefile.devel | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Makefile b/Makefile
index 7caa3434..b1c2e17f 100644
--- a/Makefile
+++ b/Makefile
@@ -79,7 +79,7 @@ compile: $(EL)
 	@echo "****************************************************************"
 	@echo " Byte compiling... "
 	@echo "****************************************************************"
-	make elc
+	$(MAKE) elc
 	@echo "****************************************************************"
 	@echo " Finished."
 	@echo "****************************************************************"
@@ -109,7 +109,7 @@ all:	compile scripts
 ## Remove generated targets
 ##
 clean:	cleanpgscripts
-	rm -f $(ELC) *~ */*~ .\#* */.\#* .byte-compile
+	rm -f $(ELC) *~ */*~ .\#* */.\#*
 	(cd doc; $(MAKE) clean)
 
 distclean: clean
@@ -199,10 +199,10 @@ install-doc: doc.info doc.pdf
 	for f in ${DOC_EXAMPLES}; do mkdir -p ${DOCDIR}/`dirname $$f`; cp -pf $$f ${DOCDIR}/$$f; done
 
 doc: FORCE
-	(cd doc; make EMACS=$(EMACS) $*)
+	(cd doc; $(MAKE) EMACS=$(EMACS) $*)
 
 doc.%: FORCE
-	(cd doc; make EMACS=$(EMACS) $*)
+	(cd doc; $(MAKE) EMACS=$(EMACS) $*)
 
 ##
 ## scripts: try to patch bash and perl scripts with correct paths
diff --git a/Makefile.devel b/Makefile.devel
index 5062c597..fac2333f 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -505,7 +505,7 @@ releaseall: release releaseclean golive
 ##	  
 golive:
 	$(GOLIVE)
-	cd $(HTMLDIR); for f in $(DOWNLOADHTMLS); do make pub.$$f; done;
+	cd $(HTMLDIR); for f in $(DOWNLOADHTMLS); do $(MAKE) pub.$$f; done;
 	rm -rf $(RELEASEDIR)
 
 
-- 
cgit v1.2.3