diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/Makefile.doc b/Makefile.doc index e89a20393c..25d146000b 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -31,8 +31,8 @@ DVIPS:=dvips HTMLSTYLE:=coqremote # Sphinx-related variables -OSNAME:=$(shell uname -o) -ifeq ($(OSNAME),Cygwin) +OSNAME:=$(shell uname -s) +ifeq ($(findstring CYGWIN,$(OSNAME)),CYGWIN) WIN_CURDIR:=$(shell cygpath -w $(CURDIR)) SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)" else @@ -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 ###################################################################### |