diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-09 13:45:35 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-10 19:23:54 +0200 |
| commit | 3d1e1adba6c6a7975ee1875d226294f5c6fb196c (patch) | |
| tree | 244ebe201bb5ce469cb81e5b1dbd72db50b75082 /Makefile.doc | |
| parent | 012ac80c38d431d68f1dacb01fbfe27bcb7f7eb0 (diff) | |
Clean-up in Makefile.doc and include Sphinx in doc-html target.
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/Makefile.doc b/Makefile.doc index c98725ad5..d13d0c09e 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -25,7 +25,6 @@ doc-no: ###################################################################### LATEX:=latex -BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 MAKEINDEX:=makeindex PDFLATEX:=pdflatex DVIPS:=dvips @@ -45,7 +44,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex ### General rules ###################################################################### -.PHONY: doc sphinxdoc-html doc-pdf doc-ps +.PHONY: doc doc-html doc-pdf doc-ps .PHONY: stdlib full-stdlib doc: sphinx stdlib @@ -57,7 +56,7 @@ sphinx: coq @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." doc-html:\ - doc/stdlib/html/index.html + doc/stdlib/html/index.html sphinx doc-pdf:\ doc/stdlib/Library.pdf @@ -79,13 +78,6 @@ full-stdlib: \ (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) ###################################################################### -# Macros for filtering outputs -###################################################################### - -HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file" -SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^ --' - -###################################################################### # Common ###################################################################### @@ -172,16 +164,17 @@ doc/stdlib/FullLibrary.pdf: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/s ###################################################################### .PHONY: install-doc install-doc-meta install-doc-html install-doc-printable \ - install-doc-index-urls install-doc-sphinx + install-doc-sphinx install-doc-stdlib-html -install-doc: install-doc-meta install-doc-html install-doc-printable \ - install-doc-index-urls install-doc-sphinx +install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: +install-doc-html: install-doc-stdlib-html install-doc-sphinx + +install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib |