From: Daniel Arndt <arndtd@ornl.gov>
Date: Wed, 4 Mar 2020 03:41:45 +0000 (-0500)
Subject: Merge pull request #9584 from tjhei/ci_jenkins_set_ex
X-Git-Tag: v9.2.0-rc1~464
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=3579e25ebac32b81091546abd0636dd01bc3df2d;p=dealii.git

Merge pull request #9584 from tjhei/ci_jenkins_set_ex

CI: Jenkins: set -x and set -e
---

3579e25ebac32b81091546abd0636dd01bc3df2d
diff --cc Jenkinsfile
index be3cc00470,8504169272..c2028333f4
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@@ -123,8 -123,13 +123,9 @@@ pipelin
              timeout(time: 6, unit: 'HOURS')
              {
                sh "echo \"building on node ${env.NODE_NAME}\""
 -              sh '''#!/bin/bash
 -                 cd $WORKSPACE/
 -                 ./contrib/utilities/check_doxygen.sh
 -              '''
                sh '''#!/bin/bash
                   set -e
+                  set -x
                   export NP=`grep -c ^processor /proc/cpuinfo`
                   export TEST_TIME_LIMIT=1200
                   mkdir -p /home/dealii/build