From 777dc33ca65659208a5ed37e33ad4127ea087436 Mon Sep 17 00:00:00 2001
From: David Aspinall
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 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Makefile')

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
-- 
cgit v1.2.3