From: Wolfgang Bangerth Date: Thu, 1 Sep 2016 01:44:11 +0000 (-0600) Subject: Merge pull request #3043 from tamiko/dealii-8.4 X-Git-Tag: v8.4.2-rc1~3 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=2487c9b9224d62d049498c84db8889190654c65e;p=dealii.git Merge pull request #3043 from tamiko/dealii-8.4 [dealii-8.4.2] Cherry pick #2933 to release branch --- 2487c9b9224d62d049498c84db8889190654c65e