aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-22 17:07:07 +0200
committerThéo Zimmermann2019-05-22 20:09:23 +0200
commit4d8a64fd4445e6a1d6a76243199f674624fa9a75 (patch)
tree3f318616a914c4a8bb3e413e22f69f0f13c6f82f /test-suite
parent5c5bd952e9c28c3acf740fcdced03b2b7145076d (diff)
Fix changelog test file on macOS: do not use ls + wc.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'test-suite')
-rwxr-xr-xtest-suite/misc/changelog.sh5
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh
index ed473e5874..76eb0de5aa 100755
--- a/test-suite/misc/changelog.sh
+++ b/test-suite/misc/changelog.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/usr/bin/env bash
if grep -q -F "is_a_released_version = False" ../config/coq_config.py; then
echo "This is not a released version: nothing to test."
@@ -7,7 +7,8 @@ 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