From 1bf651aba790afb16d21b4cd0f2d417b2a153f79 Mon Sep 17 00:00:00 2001 From: Wolfgang Bangerth Date: Fri, 28 Oct 2016 20:28:14 -0600 Subject: [PATCH] Document the purpose of the two indentation scripts in ./contrib/utilities. --- contrib/utilities/check_indentation.sh | 28 ++++++++++++++++++++++++++ contrib/utilities/indent | 13 ++++++++++++ 2 files changed, 41 insertions(+) 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 -- 2.39.5