From: Daniel Arndt 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