From 53a1fb897b8ca95c20d0d4dd54da412445a781bb Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 28 Sep 2000 12:11:35 +0000
Subject: Add default target

---
 doc/Makefile | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc/Makefile')

diff --git a/doc/Makefile b/doc/Makefile
index 0cd02947..2d008717 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -15,6 +15,9 @@
 ##
 ###########################################################################
 
+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" $@ 
-- 
cgit v1.2.3