From e9d6aef75963126d7a856f5b88db8fd1e550f596 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 7 May 2019 14:40:02 +0200
Subject: Define minimum Sphinx version in conf.py.

We set the minimum Sphinx version in conf.py to the one that we test
in our CI and the one that is documented in doc/README.md. Hopefully,
it will allow users with lower Sphinx verisons get better error
messages.
---
 doc/sphinx/conf.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/conf.py')

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 48ad60c6dd..972a53ae36 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -47,7 +47,7 @@ with open("refman-preamble.rst") as s:
 # -- General configuration ------------------------------------------------
 
 # If your documentation needs a minimal Sphinx version, state it here.
-#needs_sphinx = '1.0'
+needs_sphinx = '1.7.8'
 
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
-- 
cgit v1.2.3


From 50a89e6882e319cf6107147b49d387dd41e81805 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 8 May 2019 20:50:36 +0200
Subject: Define a new `is_a_released_version` variable in configure.ml.

Use it to not include unreleased changes when building a released
version.
---
 doc/sphinx/conf.py | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/sphinx/conf.py')

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 48ad60c6dd..25800d3a7d 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -53,6 +53,7 @@ with open("refman-preamble.rst") as s:
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
 extensions = [
+    'sphinx.ext.ifconfig',
     'sphinx.ext.mathjax',
     'sphinx.ext.todo',
     'sphinxcontrib.bibtex',
@@ -100,6 +101,7 @@ def copy_formatspecific_files(app):
 
 def setup(app):
     app.connect('builder-inited', copy_formatspecific_files)
+    app.add_config_value('coq_config', coq_config, 'env')
 
 # The master toctree document.
 # We create this file in `copy_master_doc` above.
-- 
cgit v1.2.3