doc/user: add missing sphinxcontrib.jquery

Accidentally omitted in `doc/user`, present in `doc/dev`.

diff --git a/doc/user/conf.py b/doc/user/conf.py
index fb2bd287f3a7b07e7f18228fcf127e66075c9f09..ddd3e5edfbb79728317d925207012f62a40bfe3c 100644 (file)
--- a/doc/user/conf.py
+++ b/doc/user/conf.py
@@ -24,6 +24,10 @@ extensions = [
     'sphinx_tabs.tabs',
 ]
 
+theme_major = sphinx_rtd_theme.__version__.partition('.')[0]
+if theme_major == '2':
+    extensions.append('sphinxcontrib.jquery')
+
 # List of patterns, relative to source directory, that match files and
 # directories to ignore when looking for source files.
 exclude_patterns = ['_build']