diff options
| author | Paolo G. Giarrusso | 2020-01-27 22:06:18 +0100 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2020-01-27 22:22:22 +0100 |
| commit | 8f84388e4a7fe2c64dcfbeaa6f9f5c3bf9e021b5 (patch) | |
| tree | 8cdca9d0080785eac0171499a1ef0411a9acd990 /doc | |
| parent | 614643e6fb1b5029d1c2bf50cd51f95d621010cf (diff) | |
checkdeps: check for sphinxcontrib-bibtex
I lacked this package, and got:
``` $ make -j2 COQ_USE_DUNE=1 refman-html
[...]
env doc/sphinx_build (exit 2)
(cd _build/default/doc && /usr/bin/env COQLIB=.. sphinx-build -j4 -W -b html -d sphinx_build/doctrees sphinx sphinx_build/html)
Running Sphinx v2.1.2
Extension error:
Could not import extension sphinxcontrib.bibtex (exception: No module named 'sphinxcontrib.bibtex')
make: *** [refman-html] Error 1
```
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/tools/coqrst/checkdeps.py | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py index 91f0a7cb1b..d843e73895 100644 --- a/doc/tools/coqrst/checkdeps.py +++ b/doc/tools/coqrst/checkdeps.py @@ -37,3 +37,8 @@ try: import bs4 except: missing_dep('beautifulsoup4') + +try: + import sphinxcontrib.bibtex +except: + missing_dep('sphinxcontrib-bibtex') |