From: Timo Heister <timo.heister@gmail.com>
Date: Mon, 17 Feb 2020 19:15:34 +0000 (-0500)
Subject: CI: run checkdoxygen.py for each PR
X-Git-Tag: v9.2.0-rc1~490^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=refs%2Fpull%2F9542%2Fhead;p=dealii.git

CI: run checkdoxygen.py for each PR
---

diff --git a/Jenkinsfile b/Jenkinsfile
index d74d75a8e1..104f07519a 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -123,6 +123,10 @@ 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`
diff --git a/contrib/utilities/check_doxygen.sh b/contrib/utilities/check_doxygen.sh
new file mode 100755
index 0000000000..b6ccfa2710
--- /dev/null
+++ b/contrib/utilities/check_doxygen.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+
+if [ ! -f contrib/utilities/checkdoxygen.py ]; then
+  echo "*** This script must be run from the top-level directory of deal.II."
+  exit 1
+fi
+
+
+find doc examples include \( -name "*.h" -o -name "*.dox" \) -print | xargs -n 1 contrib/utilities/checkdoxygen.py
diff --git a/contrib/utilities/check_indentation.sh b/contrib/utilities/check_indentation.sh
index 7c9fde0e5e..6ea739e9d1 100755
--- a/contrib/utilities/check_indentation.sh
+++ b/contrib/utilities/check_indentation.sh
@@ -37,3 +37,5 @@ fi
 ./contrib/utilities/indent-all || exit $?
 git diff
 git diff-files --quiet 
+
+./contrib/utilities/check_doxygen.sh || exit $?