aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-05-22 14:57:17 +0200
committerGaëtan Gilbert2019-05-22 14:57:17 +0200
commit0f16d757b67b9c7e5a1aa6c1efadd9a19a53e9db (patch)
treecc95093a05e191e2e66b329f8baa9fd7fc28fbd2 /test-suite
parente7d03413c6b8f8fbcc537a43da4c3f9ff19007ad (diff)
Use grep in changelog test instead of adhoc reads
Diffstat (limited to 'test-suite')
-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