From: Wolfgang Bangerth 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=refs%2Fpull%2F3311%2Fhead;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