From f7e17efe3abc4d20d247f3dc4d20eae2e86fcaef Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Mon, 2 Oct 2000 19:00:02 +0000
Subject: Fix recursive make

---
 doc/Makefile.doc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/Makefile.doc')

diff --git a/doc/Makefile.doc b/doc/Makefile.doc
index 75ce79cf..b1004218 100644
--- a/doc/Makefile.doc
+++ b/doc/Makefile.doc
@@ -15,8 +15,8 @@
 ##
 ###########################################################################
 
-# DOCNAME = ProofGeneral
 
+MAKE = make -f Makefile.doc 
 MAKEINFO = makeinfo
 TEXI2DVI = texi2dvi
 
@@ -51,7 +51,7 @@ default: doc
 
 .texi.dvi:
 	$(TEXI2DVI) $<
-	if `which $(DVISELECT) > /dev/null`; then $(MAKE) rearrange; fi
+	if `which $(DVISELECT) > /dev/null`; then $(MAKE) rearrange DOCNAME=$*; fi
 
 rearrange:
 	$(DVISELECT) -i $(DOCNAME).dvi -o $(DOCNAME).tmp1 $(TITLERANGE)
-- 
cgit v1.2.3