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.devel | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.devel')

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