]> https://gitweb.dealii.org/ - dealii.git/commit
Merge pull request #10383 from tjhei/github-actions-no-indent
authorMatthias Maier <tamiko@43-1.org>
Wed, 27 May 2020 17:09:14 +0000 (12:09 -0500)
committerGitHub <noreply@github.com>
Wed, 27 May 2020 17:09:14 +0000 (12:09 -0500)
commite38d0909f0beaa20961d3eabcc005e424f15417d
tree42b72f03cfdf9cfff3bd7e507d5d2a58f9ffa554
parentc6a4a5438f3b1cbef76a084d89614a8d33fbff60
parent89c52791ec65c6e9d0ebb4ba52ca0f8f168e39f5
Merge pull request #10383 from tjhei/github-actions-no-indent

[CI] github actions do not check indent

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.