commit 423553e2d91517c8b6e456fa87ef15225c1a1eec
author Davide Pesavento <davidepesa@gmail.com> Fri Aug 19 20:46:06 2022 -0400
committer Davide Pesavento <davidepesa@gmail.com> Fri Aug 19 20:46:06 2022 -0400
tree ed655b6f090232d85c637f15513cfb9debf364e8
parent 38fd3987c904514efcbd87064e96b7004b72f344

build+ci: support CentOS Stream 9 and macOS/arm64

This commit also syncs the CI config and scripts with ndn-tools

Change-Id: I58246dac18b262d23404d12292988ef34d49525a

.jenkins.d/30-coverage.sh

diff --git a/.jenkins.d/30-coverage.sh b/.jenkins.d/30-coverage.sh
index 5d74ff8..eb100d3 100755
--- a/.jenkins.d/30-coverage.sh
+++ b/.jenkins.d/30-coverage.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -ex
+set -exo pipefail
 
 if [[ $JOB_NAME == *"code-coverage" ]]; then
     # Generate an XML report (Cobertura format) and a detailed HTML report using gcovr