aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-22 17:39:32 +0200
committerThéo Zimmermann2019-05-22 17:39:32 +0200
commit4f2e05f5abc19addc25501281b4cd34ed5e33853 (patch)
treed83576e50eebb0fae662e1f8412383ffce0d3ac6
parent049cfe725d334fb863df31ee9e03db4b54a64455 (diff)
parent0f16d757b67b9c7e5a1aa6c1efadd9a19a53e9db (diff)
Merge PR #10211: Use grep in changelog test instead of adhoc reads
Reviewed-by: Zimmi48
-rwxr-xr-xtest-suite/misc/changelog.sh6
1 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh
index 8b4a49e577..ed473e5874 100755
--- a/test-suite/misc/changelog.sh
+++ b/test-suite/misc/changelog.sh
@@ -1,11 +1,9 @@
#!/bin/sh
-while read line; do
- if [ "$line" = "is_a_released_version = False" ]; then
+if grep -q -F "is_a_released_version = False" ../config/coq_config.py; then
echo "This is not a released version: nothing to test."
exit 0
- fi
-done < ../config/coq_config.py
+fi
for d in ../doc/changelog/*; do
if [ -d "$d" ]; then