diff options
| author | Gaëtan Gilbert | 2019-02-07 11:42:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-12 14:39:49 +0100 |
| commit | 146a9d73bd5ceff18e08d36d942dca874f388d5c (patch) | |
| tree | 08c79cb48e8831a3e0d3c28f6a995a20e9e1e926 /Makefile.doc | |
| parent | 912e363c9152012ecbff5272cded46e75a2f3c33 (diff) | |
Fix undefined SPHINX_DEPS when QUICK
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.doc b/Makefile.doc index 7ac710b8c9..4b2dd8ed4d 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -54,6 +54,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex doc: refman stdlib +SPHINX_DEPS ?= ifndef QUICK SPHINX_DEPS := coq endif |