From 71c2a96eee865be6c4f8ccccd97ab284a6313842 Mon Sep 17 00:00:00 2001 From: Wolfgang Bangerth Date: Tue, 23 Apr 2019 16:18:55 -0600 Subject: [PATCH] Fix a grammar mistake in a comment. --- contrib/utilities/indent_common.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 # -- 2.39.5