From: Matthias Maier <tamiko@43-1.org>
Date: Wed, 20 Jun 2018 22:03:24 +0000 (-0500)
Subject: contrib: update auxiliary scripts
X-Git-Tag: v9.1.0-rc1~1007^2~2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=b1b740adadef6bdce9c9023072a7bdb3b1bad5c7;p=dealii.git

contrib: update auxiliary scripts
---

diff --git a/contrib/git-hooks/pre-commit b/contrib/git-hooks/pre-commit
index fe8b9aae6f..54c0655016 100755
--- a/contrib/git-hooks/pre-commit
+++ b/contrib/git-hooks/pre-commit
@@ -20,18 +20,18 @@
 
 BASEDIR="$(git rev-parse --show-toplevel 2>/dev/null)"
 
-if [ ! -f "${BASEDIR}"/contrib/utilities/indent-branch ]; then
+if [ ! -f "${BASEDIR}"/contrib/utilities/indent ]; then
   echo "*** This script must be run from within the deal.II git repository."
   exit 1
 fi
 
 cd "${BASEDIR}"
-OUTPUT="$(REPORT_ONLY=true "${BASEDIR}"/contrib/utilities/indent-branch)"
+OUTPUT="$(REPORT_ONLY=true "${BASEDIR}"/contrib/utilities/indent)"
 
 if [ ! -z "${OUTPUT}" ]; then
   echo "git commit aborted due to formatting issues:"
   echo "${OUTPUT}"
   echo ""
-  echo "Please run ./contrib/utilities/indent-branch to fix these issues and try again."
+  echo "Please run ./contrib/utilities/indent to fix these issues and try again."
   exit 1
 fi
diff --git a/contrib/utilities/check_indentation.sh b/contrib/utilities/check_indentation.sh
index fa81f582f7..a14a67859a 100755
--- a/contrib/utilities/check_indentation.sh
+++ b/contrib/utilities/check_indentation.sh
@@ -34,6 +34,6 @@ else
 	echo "Running indentation test on Pull Request #${TRAVIS_PULL_REQUEST}"
 fi
 
-./contrib/utilities/indent
+./contrib/utilities/indent-all
 git diff
 git diff-files --quiet