aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/conf.py
diff options
context:
space:
mode:
authorClément Pit-Claudel2020-03-23 16:02:42 -0400
committerClément Pit-Claudel2020-03-23 16:02:42 -0400
commitf4b9158addf87e48a5287e400a8858406f20655e (patch)
tree8d3e988d6756fb838c017c79d9fd822310bc2c8e /doc/sphinx/conf.py
parent47d92a69773755e2ad5d5f987f87337fdf7e98d8 (diff)
[refman] Fix caching, which was broken by the addition of coq_config
Diffstat (limited to 'doc/sphinx/conf.py')
-rwxr-xr-xdoc/sphinx/conf.py2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 3d77d07061..4bf1a6f3a9 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -100,7 +100,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')
+ app.add_config_value('is_a_released_version', coq_config.is_a_released_version, 'env')
# The master toctree document.
# We create this file in `copy_master_doc` above.