diff options
| author | Vincent Laporte | 2019-05-24 08:13:10 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-24 08:13:10 +0000 |
| commit | 1c2cfc1fc66416dbd72dc5f1c72b608727195b27 (patch) | |
| tree | 19d761fa47bf0cd7c794eb45f49d25eb000167b1 | |
| parent | f6aeed0b7de9581200749f9ded48360540ce8471 (diff) | |
| parent | 056d1c3a9f5e220c2ad9877c87a559fc454b7d0f (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/dune | 1 | ||||
| -rwxr-xr-x | test-suite/misc/changelog.sh | 5 |
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 |
