diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-06 16:32:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-12 14:56:47 +0200 |
| commit | 556bcae1d29707b21a527a134d38a94623abf5dd (patch) | |
| tree | 86ada5bd96229f1f6d1e6b2469b822c99240d1a8 /Makefile.doc | |
| parent | 7dd881fc72d62eb0c1f1e5063eb3a8ed268fb5d5 (diff) | |
Sphinx: a "QUICK=1" option to bypass recompilation of the library.
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index d13d0c09e..41ae11b86 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -49,7 +49,11 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex doc: sphinx stdlib -sphinx: coq +ifndef QUICK +SPHINX_DEPS := coq +endif + +sphinx: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx' $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html @echo |