]> https://gitweb.dealii.org/ - dealii.git/commit
Merge pull request #11048 from peterrum/gc_remove_include
authorTimo Heister <timo.heister@gmail.com>
Fri, 16 Oct 2020 20:23:35 +0000 (16:23 -0400)
committerGitHub <noreply@github.com>
Fri, 16 Oct 2020 20:23:35 +0000 (16:23 -0400)
commitec22a073aacb5f9ed8d4b1ceab681b93ef94eb0d
tree95daeb950dc4c97626718e77d49ad559f3bb21f9
parentb720078b8eda3b250e305067ffd0eaac835db0b7
parentfad4f03835030cf5b1c3450bc4d790719c434c43
Merge pull request #11048 from peterrum/gc_remove_include

Remove unnecessary include

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.