From: Martin Kronbichler Date: Thu, 6 Aug 2015 13:42:14 +0000 (+0200) Subject: Merge pull request #1283 from bangerth/fix-warning-2 X-Git-Tag: v8.4.0-rc2~663 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=5fe249fe7051a8184617b3278cff9d9fa760e706;p=dealii.git Merge pull request #1283 from bangerth/fix-warning-2 Avoid a warning. --- 5fe249fe7051a8184617b3278cff9d9fa760e706