Merge PR #10085: Do not include unreleased changelog in released versions.

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: vbgl

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh
new file mode 100755
index 0000000000..8b4a49e577
--- /dev/null
+++ b/test-suite/misc/changelog.sh
@@ -0,0 +1,18 @@
+#!/bin/sh
+
+while read line; do
+  if [ "$line" = "is_a_released_version = False" ]; then
+    echo "This is not a released version: nothing to test."
+    exit 0
+  fi
+done < ../config/coq_config.py
+
+for d in ../doc/changelog/*; do
+  if [ -d "$d" ]; then
+    if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then
+      echo "Fatal: unreleased changelog entries remain in ${d#../}/"
+      echo "Include them in doc/sphinx/changes.rst and remove them from doc/changelog/"
+      exit 1
+    fi
+  fi
+done