diff options
| author | Théo Zimmermann | 2019-02-13 11:49:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-13 11:49:29 +0100 |
| commit | 90e2fa3344cff478a2ab23c0dbbb5eab5b4668e4 (patch) | |
| tree | 7ad437364d4998e8a95ee8c0d1a1827099bd8084 /Makefile.doc | |
| parent | 0b0fa735dc0da5660a870053a5a5f6fd1c5e22d1 (diff) | |
| parent | d638148dc3e0220ac99761cf9f2efa8284882c41 (diff) | |
Merge PR #9553: Sphinx various fixing of failing commands
Ack-by: Zimmi48
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 |