]> https://gitweb.dealii.org/ - dealii.git/commit
Merge pull request #12516 from drwells/cherry-pick-12511
authorMatthias Maier <tamiko@43-1.org>
Mon, 28 Jun 2021 20:51:32 +0000 (15:51 -0500)
committerGitHub <noreply@github.com>
Mon, 28 Jun 2021 20:51:32 +0000 (15:51 -0500)
commitd68635b7fee696bfc5975ef4ec7cff88379d7774
tree435c56b42ff4421893e9ff6ae1df712fec130041
parentbd94e14734e9adf14a87b591bfa5a945a71d8439
parente3e15f172757ce4ec0104b5f8e8e0c2f607ea27d
Merge pull request #12516 from drwells/cherry-pick-12511

[9.3] take over #12511 - add one more missing file extension.

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.