From: Timo Heister <timo.heister@gmail.com>
Date: Sun, 1 Mar 2020 17:50:06 +0000 (-0500)
Subject: CI: remove check_doxygen as we do this in Travis
X-Git-Tag: v9.2.0-rc1~486^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=refs%2Fpull%2F9583%2Fhead;p=dealii.git

CI: remove check_doxygen as we do this in Travis

see #9582
---

diff --git a/Jenkinsfile b/Jenkinsfile
index a80e466537..be3cc00470 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -123,10 +123,6 @@ pipeline
             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
                  export NP=`grep -c ^processor /proc/cpuinfo`