]> https://gitweb.dealii.org/ - dealii.git/commitdiff
CI: check file encoding 9711/head
authorTimo Heister <timo.heister@gmail.com>
Sun, 22 Mar 2020 14:38:31 +0000 (10:38 -0400)
committerTimo Heister <timo.heister@gmail.com>
Sun, 22 Mar 2020 14:38:31 +0000 (10:38 -0400)
closes #8076

contrib/utilities/check_indentation.sh

index f2a353ef91d048c359a7df3094ba91e590aa127d..ad8207b77e229672b89ddfaebb4a6e13fa4f3ee1 100755 (executable)
@@ -43,5 +43,8 @@ git diff-files --quiet || exit $?
 # Run various checks involving doxygen documentation:
 ./contrib/utilities/check_doxygen.sh || exit $?
 
+# Check for utf8 encoding:
+./contrib/utilities/check_encoding.py || exit $?
+
 # Success!
 exit 0

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.