]> https://gitweb.dealii.org/ - dealii.git/commitdiff
[CI] github actions do not check indent 10383/head
authorTimo Heister <timo.heister@gmail.com>
Wed, 27 May 2020 14:13:55 +0000 (10:13 -0400)
committerTimo Heister <timo.heister@gmail.com>
Wed, 27 May 2020 14:14:10 +0000 (10:14 -0400)
.github/workflows/main.yml

index baeeedb23a0dcc73fc2f88755cb6be40c76e34e6..460661c319f0936f7a7739e81a89544394662637 100644 (file)
@@ -28,7 +28,6 @@ jobs:
         path: detailed.log
     - name: build
       run: |
-        ./contrib/utilities/check_indentation.sh
         make -j 2
 
   osx-serial:
@@ -56,7 +55,6 @@ jobs:
         path: detailed.log
     - name: build
       run: |
-        ./contrib/utilities/check_indentation.sh
         make -j 2
         make -j 2 test # quicktests
 
@@ -92,7 +90,6 @@ jobs:
         path: detailed.log
     - name: build
       run: |
-        ./contrib/utilities/check_indentation.sh
         make -j 2
         make -j 2 test #quicktests
 

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.