From 586d6add6d2d4405eacf9241ee0d55f58435e364 Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 17 Oct 2008 14:06:04 +0000
Subject: Suppression de la dépendance de install-doc envers doc :   - make
 install ne compile plus la doc   - make world compile la doc (sauf si option
 --with-doc no)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11460 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 6 ++++--
 Makefile.doc   | 4 ++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index a159fc95f9..872f8e30bd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -34,11 +34,13 @@ endif
 NOARG: world
 
 # build and install the three subsystems: coq, coqide, pcoq
-world: revision coq coqide pcoq
-
 ifeq ($(WITHDOC),all)
+world: revision coq coqide pcoq doc
+
 install: install-coq install-coqide install-pcoq install-doc
 else
+world: revision coq coqide pcoq
+
 install: install-coq install-coqide install-pcoq
 endif
 
diff --git a/Makefile.doc b/Makefile.doc
index 89a2290b2a..d8ef102937 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -224,7 +224,7 @@ install-doc-meta:
 	$(MKDIR) $(FULLDOCDIR)
 	$(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc
 
-install-doc-html: doc-html
+install-doc-html: 
 	$(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq)
 	$(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman 
 	$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib 
@@ -232,7 +232,7 @@ install-doc-html: doc-html
 	$(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html
 
-install-doc-printable: doc-pdf doc-ps
+install-doc-printable: 
 	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
 	$(INSTALLLIB) doc/refman/Reference-Manual.pdf \
 		doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
-- 
cgit v1.2.3