diff options
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/Makefile b/doc/Makefile index 4c29a546..0331cd10 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -19,13 +19,13 @@ default: $(MAKE) doc %: - make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" $@ - make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" $@ + $(MAKE) -f Makefile.doc DOCNAME=PG-adapting MAKE="$(MAKE) -f Makefile.doc" $@ + $(MAKE) -f Makefile.doc DOCNAME=ProofGeneral MAKE="$(MAKE) -f Makefile.doc" $@ ## ## man page for proofgeneral script ## # man: proofgeneral.1 # -#proofgeneral.1: ../bin/proofgeneral -# help2man --output=$@ ../bin/proofgeneral +proofgeneral.1: ../bin/proofgeneral + help2man --output=$@ ../bin/proofgeneral |