]> https://gitweb.dealii.org/ - dealii.git/commit
CI: change git depth for indent worker
authorTimo Heister <timo.heister@gmail.com>
Fri, 31 Jul 2020 14:11:00 +0000 (10:11 -0400)
committerTimo Heister <timo.heister@gmail.com>
Fri, 31 Jul 2020 14:27:44 +0000 (10:27 -0400)
commit183db476e2a70a85025a8830c9e99f513f103ec8
tree8eb6298b4d7e6c4c9527e8f24ec782e501b1ddd9
parenta6e0cd02792b729fee27a88d16bf4870a407530c
CI: change git depth for indent worker

By default, github actions do a git clone with depth=1. That does not
allow our indent script to check the commits for authorship correctly.
.github/workflows/indent.yml

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.