diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/Makefile.doc b/Makefile.doc index 8e958532f0..50c4acb416 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -71,7 +71,10 @@ refman-%: $(SPHINX_DEPS) doc/unreleased.rst $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* +COQREFMAN_FILES := $(wildcard $(SPHINXBUILDDIR)/latex/CoqRefMan*) +LATEX_REMOVE_FILES := $(filter-out $(SPHINXBUILDDIR)/latex/CoqRefMan.tex, $(COQREFMAN_FILES)) refman-pdf: refman-latex + rm -f $(LATEX_REMOVE_FILES) +$(MAKE) -C $(SPHINXBUILDDIR)/latex refman: $(SPHINX_DEPS) @@ -126,6 +129,8 @@ doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst) # Standard library ###################################################################### +DOCLIBS=-R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 + ### Standard library (browsable html format) ifdef QUICK @@ -136,7 +141,7 @@ endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ - -R theories Coq -R plugins Coq $(VFILES) + $(DOCLIBS) $(VFILES) mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index @@ -175,12 +180,12 @@ doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex ifdef QUICK doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp else doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO) $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp endif |