]> https://gitweb.dealii.org/ - dealii.git/commit
projects / dealii.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a6e0cd0) | patch
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
tree8eb6298b4d7e6c4c9527e8f24ec782e501b1ddd9tree | snapshot
parenta6e0cd02792b729fee27a88d16bf4870a407530ccommit | diff
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 diff | blob | history
Mirror of the development repository for deal.II

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.