]> https://gitweb.dealii.org/ - dealii.git/commit
Merge pull request #10491 from tjhei/github_actions_indent
authorDaniel Arndt <arndtd@ornl.gov>
Wed, 10 Jun 2020 17:42:09 +0000 (13:42 -0400)
committerGitHub <noreply@github.com>
Wed, 10 Jun 2020 17:42:09 +0000 (13:42 -0400)
commit286f685f7bef5cbb5ce2d48df2d2a6cca4c84b99
treef6f94e05269e18fd26834ed7a6819efe0f2f1a75
parent7d56595d24438b5e2ae032cc7c7d9ec36a192eee
parent0434c84e74f6dff5fd50a09a18aec12a4fff7f9e
Merge pull request #10491 from tjhei/github_actions_indent

[CI] add githubactions indent/documentation check

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.