From 8f84388e4a7fe2c64dcfbeaa6f9f5c3bf9e021b5 Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Mon, 27 Jan 2020 22:06:18 +0100
Subject: 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
```
---
 doc/tools/coqrst/checkdeps.py | 5 +++++
 1 file changed, 5 insertions(+)

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')
-- 
cgit v1.2.3