From 443e9dbde4f48b9ba53ad76236fbe65353c3b029 Mon Sep 17 00:00:00 2001
From: Timo Heister <timo.heister@gmail.com>
Date: Mon, 17 Feb 2020 14:15:34 -0500
Subject: [PATCH] CI: run checkdoxygen.py for each PR

---
 Jenkinsfile                            | 4 ++++
 contrib/utilities/check_doxygen.sh     | 9 +++++++++
 contrib/utilities/check_indentation.sh | 2 ++
 3 files changed, 15 insertions(+)
 create mode 100755 contrib/utilities/check_doxygen.sh

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 $?
-- 
2.39.5