From 65e1d85aa03563c8ef25a87babb62367806c1352 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 21 Sep 2000 16:57:03 +0000 Subject: Make PG-adapting first so index.html left pointing to main manual --- doc/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/Makefile') diff --git a/doc/Makefile b/doc/Makefile index 3ee3ee9a..0cd02947 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -16,6 +16,6 @@ ########################################################################### %: - 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" $@ -- cgit v1.2.3