From: Wolfgang Bangerth <bangerth@colostate.edu>
Date: Sat, 29 Oct 2016 02:28:14 +0000 (-0600)
Subject: Document the purpose of the two indentation scripts in ./contrib/utilities.
X-Git-Tag: v8.5.0-rc1~527^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=1bf651aba790afb16d21b4cd0f2d417b2a153f79;p=dealii.git

Document the purpose of the two indentation scripts in ./contrib/utilities.
---

diff --git a/contrib/utilities/check_indentation.sh b/contrib/utilities/check_indentation.sh
index 7a859c98e3..1f1daa199c 100755
--- a/contrib/utilities/check_indentation.sh
+++ b/contrib/utilities/check_indentation.sh
@@ -1,4 +1,32 @@
 #!/bin/sh
+## ---------------------------------------------------------------------
+##
+## Copyright (C) 2014 - 2016 by the deal.II authors
+##
+## This file is part of the deal.II library.
+##
+## The deal.II library is free software; you can use it, redistribute
+## it, and/or modify it under the terms of the GNU Lesser General
+## Public License as published by the Free Software Foundation; either
+## version 2.1 of the License, or (at your option) any later version.
+## The full text of the license can be found in the file LICENSE at
+## the top level of the deal.II distribution.
+##
+## ---------------------------------------------------------------------
+
+#
+# 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.
+#
+# 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.
+#
 
 if [ "${TRAVIS_PULL_REQUEST}" = "false" ]; then 
 	echo "Running indentation test on master merge."
diff --git a/contrib/utilities/indent b/contrib/utilities/indent
index 6278491eea..78a7263cfb 100755
--- a/contrib/utilities/indent
+++ b/contrib/utilities/indent
@@ -14,6 +14,19 @@
 ##
 ## ---------------------------------------------------------------------
 
+#
+# This script indents all source files of deal.II according to our
+# usual code formatting standards. It is used to ensure that our
+# code base looks uniform, as uniformity helps make code easier to
+# read.
+#
+# The script needs to be executed as 
+#   ./contrib/utilities/indent
+# from the top-level directory of the source tree, or via
+#   make indent
+# from a build directory.
+#
+
 if test ! -d source -o ! -d include -o ! -d examples ; then
   echo "*** This script must be run from the top-level directory of deal.II."
   exit 1