aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorVincent Laporte2019-05-24 08:13:10 +0000
committerVincent Laporte2019-05-24 08:13:10 +0000
commit1c2cfc1fc66416dbd72dc5f1c72b608727195b27 (patch)
tree19d761fa47bf0cd7c794eb45f49d25eb000167b1
parentf6aeed0b7de9581200749f9ded48360540ce8471 (diff)
parent056d1c3a9f5e220c2ad9877c87a559fc454b7d0f (diff)
Merge PR #10163: Fix dependencies of new test file and fix macOS issues.
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl
-rw-r--r--test-suite/dune1
-rwxr-xr-xtest-suite/misc/changelog.sh5
2 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/dune b/test-suite/dune
index cd33319fa4..041c181d66 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -22,6 +22,7 @@
../doc/stdlib/index-list.html.template
; For the changelog test
../config/coq_config.py
+ (source_tree doc/changelog)
(package coq)
; For fake_ide
(package coqide-server)
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