diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-17 14:06:04 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-17 14:06:04 +0000 |
| commit | 586d6add6d2d4405eacf9241ee0d55f58435e364 (patch) | |
| tree | af400cb8db0f892e4940cf121ae8687fadfbe938 | |
| parent | 7829e141667c7083acc1ddfb10ddf2574c3ca0e5 (diff) | |
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
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rw-r--r-- | Makefile.doc | 4 |
2 files changed, 6 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build index a159fc95f..872f8e30b 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 89a2290b2..d8ef10293 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 |