]> https://gitweb.dealii.org/ - dealii.git/commitdiff
Fix a grammar mistake in a comment. 7951/head
authorWolfgang Bangerth <bangerth@colostate.edu>
Tue, 23 Apr 2019 22:18:55 +0000 (16:18 -0600)
committerWolfgang Bangerth <bangerth@colostate.edu>
Tue, 23 Apr 2019 22:18:55 +0000 (16:18 -0600)
contrib/utilities/indent_common.sh

index 6bbeb92115abb20494d4d60885b4dbf64d17903d..c8e4a26f96072be0e10c0c9ae37374bad1135784 100644 (file)
@@ -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
 #

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.