aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1998-09-23 11:07:06 +0000
committerDavid Aspinall1998-09-23 11:07:06 +0000
commitcdb54a33c37ced8f90549c2b760988d15fbeffaf (patch)
tree46bd3eedfa359d60696309c65fdb000ba9fa99a7
parent7c7ce3612b2c4d864c77cd3ffb6c16ee15e07cfb (diff)
Added FORCE dependency for docs.
-rw-r--r--Makefile.devel4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel
index d47915e7..430a59f1 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -123,10 +123,10 @@ distclean: clean
#
# Documentation
#
-doc:
+doc: FORCE
(cd doc; $(MAKE) doc)
-alldocs:
+alldocs: FORCE
(cd doc; $(MAKE) all)