diff options
| author | Théo Zimmermann | 2019-05-22 17:39:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-22 17:39:32 +0200 |
| commit | 4f2e05f5abc19addc25501281b4cd34ed5e33853 (patch) | |
| tree | d83576e50eebb0fae662e1f8412383ffce0d3ac6 | |
| parent | 049cfe725d334fb863df31ee9e03db4b54a64455 (diff) | |
| parent | 0f16d757b67b9c7e5a1aa6c1efadd9a19a53e9db (diff) | |
Merge PR #10211: Use grep in changelog test instead of adhoc reads
Reviewed-by: Zimmi48
| -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 |
