diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-10-02 19:00:02 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-10-02 19:00:02 +0000 |
| commit | f7e17efe3abc4d20d247f3dc4d20eae2e86fcaef (patch) | |
| tree | 01105e1bb0543c851f848d2a9c5cd5f87fd5922c /doc/Makefile.doc | |
| parent | e29b59785cfc57c96725901692a091ac2102ce12 (diff) | |
Fix recursive make
Diffstat (limited to 'doc/Makefile.doc')
| -rw-r--r-- | doc/Makefile.doc | 4 |
1 files changed, 2 insertions, 2 deletions
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) |