From: Wolfgang Bangerth Date: Tue, 23 Apr 2019 22:18:55 +0000 (-0600) Subject: Fix a grammar mistake in a comment. X-Git-Tag: v9.1.0-rc1~186^2 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=71c2a96eee865be6c4f8ccccd97ab284a6313842;p=dealii.git Fix a grammar mistake in a comment. --- diff --git a/contrib/utilities/indent_common.sh b/contrib/utilities/indent_common.sh index 6bbeb92115..c8e4a26f96 100644 --- a/contrib/utilities/indent_common.sh +++ b/contrib/utilities/indent_common.sh @@ -205,7 +205,7 @@ export -f fix_permissions # serves as a good candidate to separate individual file names. # - For 'xargs', -0 does the opposite: it separates filenames that are # delimited by \0 -# - the options "-n 1 -P 10" make sure that the following script with be +# - the options "-n 1 -P 10" make sure that the following script will be # called exactly with one file name as argument at a time, but we allow # execution for up to 10 times in parallel #