diff options
| author | Emilio Jesus Gallego Arias | 2020-01-17 04:57:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-17 18:02:55 +0100 |
| commit | c3cf1451e6a07a30f58b5704474b19ce7feb1afa (patch) | |
| tree | 0947101869a02b1b4403593341e9adf0acb6c719 /Makefile.doc | |
| parent | a47e2f6587e3507a12d4d86b9769b93e01023350 (diff) | |
[doc] [ltac2] Build Ltac2 documentation [make build system]
Build and install the Ltac2 documentation.
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 |