diff options
| author | Gaëtan Gilbert | 2019-05-22 14:57:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-22 14:57:17 +0200 |
| commit | 0f16d757b67b9c7e5a1aa6c1efadd9a19a53e9db (patch) | |
| tree | cc95093a05e191e2e66b329f8baa9fd7fc28fbd2 /test-suite | |
| parent | e7d03413c6b8f8fbcc537a43da4c3f9ff19007ad (diff) | |
Use grep in changelog test instead of adhoc reads
Diffstat (limited to 'test-suite')
| -rwxr-xr-x | test-suite/misc/changelog.sh | 6 |
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 |
