diff options
| author | Théo Zimmermann | 2019-05-08 20:50:36 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-08 20:50:36 +0200 |
| commit | 50a89e6882e319cf6107147b49d387dd41e81805 (patch) | |
| tree | fa70140d4824adb07a2ed70c6ed17de57e247b69 /doc/sphinx/changes.rst | |
| parent | e30d52a3c724a71bf43b46416c09e4b6ef1d1f67 (diff) | |
Define a new `is_a_released_version` variable in configure.ml.
Use it to not include unreleased changes when building a released
version.
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5704587ae0..574b943a78 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2,7 +2,9 @@ Recent changes -------------- -.. include:: ../unreleased.rst +.. ifconfig:: not coq_config.is_a_released_version + + .. include:: ../unreleased.rst Version 8.10 ------------ |