From 3d1e1adba6c6a7975ee1875d226294f5c6fb196c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Wed, 9 May 2018 13:45:35 +0200
Subject: Clean-up in Makefile.doc and include Sphinx in doc-html target.

---
 Makefile.doc | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

(limited to 'Makefile.doc')

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
@@ -78,13 +77,6 @@ full-stdlib: \
 %.ps: %.dvi
 	(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
 
-- 
cgit v1.2.3