diff options
Diffstat (limited to 'test-suite/misc')
| -rwxr-xr-x | test-suite/misc/changelog.sh | 11 | ||||
| -rwxr-xr-x | test-suite/misc/printers.sh | 8 |
2 files changed, 12 insertions, 7 deletions
diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh index 8b4a49e577..76eb0de5aa 100755 --- a/test-suite/misc/changelog.sh +++ b/test-suite/misc/changelog.sh @@ -1,15 +1,14 @@ -#!/bin/sh +#!/usr/bin/env bash -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 - if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then + files=("$d"/*.rst) + if [ "${#files[@]}" != 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 diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index ef3f056d89..f659fce680 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,2 +1,8 @@ #!/bin/sh -if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi + +command -v "${BIN}coqtop.byte" || { echo "Missing coqtop.byte"; exit 1; } + +f=$(mktemp) +printf 'Drop. #use"include";; #quit;;\n' | "${BIN}coqtop.byte" -q 2>&1 | tee "$f" + +if grep -q -E "Error|Unbound" "$f"; then exit 1; fi |