diff options
| author | Théo Zimmermann | 2020-01-17 19:37:58 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-17 19:37:58 +0100 |
| commit | 1f3ad4f8ebbf48d68488d19335d3c2db18e248f4 (patch) | |
| tree | 349f615d456252c593e4a0512de732c914fa9903 /Makefile.doc | |
| parent | 58a9fa018995aa59e30bb7156a6c91b640f88730 (diff) | |
| parent | c3cf1451e6a07a30f58b5704474b19ce7feb1afa (diff) | |
Merge PR #11413: [doc] [ltac2] Build Ltac2 documentation
Reviewed-by: Zimmi48
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Makefile.doc b/Makefile.doc index 125a4b33d5..50c4acb416 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -129,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 @@ -139,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 @@ -178,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 |