From 4d8a64fd4445e6a1d6a76243199f674624fa9a75 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 22 May 2019 17:07:07 +0200
Subject: Fix changelog test file on macOS: do not use ls + wc.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
---
 test-suite/misc/changelog.sh | 5 +++--
 1 file 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
-- 
cgit v1.2.3


From 056d1c3a9f5e220c2ad9877c87a559fc454b7d0f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 14 May 2019 13:49:00 +0200
Subject: Fix dependencies of new test file.

---
 test-suite/dune | 1 +
 1 file changed, 1 insertion(+)

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)
-- 
cgit v1.2.3