cleanup and document check_indentation.sh

diff --git a/contrib/utilities/check_indentation.sh b/contrib/utilities/check_indentation.sh
index fb5fa97f11fc0b7c6b36518dd22b78f8a472ee20..f2a353ef91d048c359a7df3094ba91e590aa127d 100755 (executable)
--- a/contrib/utilities/check_indentation.sh
+++ b/contrib/utilities/check_indentation.sh
@@ -17,15 +17,12 @@
 #
 # This is a script that is used by the continuous integration servers
 # to make sure that the currently checked out version of a git repository
-# satisfies our indentation standards.
+# satisfies our "indentation" standards. This does no longer only cover
+# indentation, but other automated checks as well.
 #
-# It does so by running the 'indent' script (located in the current
-# directory), calling 'git diff' to show what differences exist between
-# the correctly indented code and what is in the git index (which is
-# typically what is in the last commit), and then running a command
-# that either returns success or failure, depending on whether or not
-# there are differences. The continuous integration services return
-# a failure code for a pull request if this script returns a failure.
+# WARNING: The continuous integration services return a failure code for a
+# pull request if this script returns a failure, so the return value of this
+# script is important.
 #
 
 if [ "${TRAVIS_PULL_REQUEST}" = "false" ]; then 
@@ -34,8 +31,17 @@ else
        echo "Running indentation test on Pull Request #${TRAVIS_PULL_REQUEST}"
 fi
 
+# Run indent-all and fail if script fails:
 ./contrib/utilities/indent-all || exit $?
+
+# Show the diff in the output:
 git diff
+
+# Make this script fail if any changes were applied by indent above:
 git diff-files --quiet || exit $?
 
+# Run various checks involving doxygen documentation:
 ./contrib/utilities/check_doxygen.sh || exit $?
+
+# Success!
+exit 0