From: Martin Kronbichler Date: Sat, 4 Apr 2020 21:12:25 +0000 (+0200) Subject: Merge pull request #9799 from bangerth/cleanup X-Git-Tag: v9.2.0-rc1~296 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=bf171735d87b844042fee782df90a2ab09b14fbf;p=dealii.git Merge pull request #9799 from bangerth/cleanup Minor cleanups. --- bf171735d87b844042fee782df90a2ab09b14fbf