diff options
| author | Enrico Tassi | 2019-05-04 14:18:22 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-05 19:23:27 +0200 |
| commit | d50433a9ca321ed0b28996567f72ac9654bf4422 (patch) | |
| tree | c94c95d5ce92951c52ff4ea394b24ee6f23104f9 | |
| parent | 81301b55df9c52fe5503421eb9527bb04a1643e0 (diff) | |
[make] build unreleased.rst
| -rw-r--r-- | Makefile.doc | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index 23aa66a1b8..25d146000b 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -66,7 +66,7 @@ SPHINX_DEPS := coq endif # refman-html and refman-latex -refman-%: $(SPHINX_DEPS) +refman-%: $(SPHINX_DEPS) doc/unreleased.rst $(SHOW)'SPHINXBUILD doc/sphinx ($*)' $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* @@ -116,6 +116,12 @@ plugin-tutorial: states tools doc/common/version.tex: config/Makefile printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.tex +### Changelog + +doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst) + $(SHOW)'AGGREGATE $@' + $(HIDE)cat doc/changelog/00-title.rst doc/changelog/*/*.rst > $@ + ###################################################################### # Standard library ###################################################################### |