commit 69857c37c29a0add683d40a96dc7c06f348799ff
author Davide Pesavento <davidepesa@gmail.com> Sun Apr 05 16:36:26 2020 -0400
committer Davide Pesavento <davidepesa@gmail.com> Mon Apr 06 15:32:21 2020 -0400
tree 44973157f7aad6bd3f142e111bc639d54243c973
parent feeb918ea8664dab421630a908f1b3b0db922857

build+docs: switch to python3, refresh FAQ and INSTALL documents

Refs: #5095
Change-Id: Icdc0e9463b28c07783edbe392a9bc47136947e3b

.jenkins.d/30-coverage.sh

diff --git a/.jenkins.d/30-coverage.sh b/.jenkins.d/30-coverage.sh
index 0dbb03a..380366e 100755
--- a/.jenkins.d/30-coverage.sh
+++ b/.jenkins.d/30-coverage.sh
@@ -1,10 +1,5 @@
 #!/usr/bin/env bash
-set -e
-
-JDIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
-source "$JDIR"/util.sh
-
-set -x
+set -ex
 
 if [[ $JOB_NAME == *"code-coverage" ]]; then
     gcovr --object-directory=build \