From: Matthias Maier Date: Mon, 19 Jan 2015 23:10:04 +0000 (+0100) Subject: Merge pull request #457 from tamiko/dealii-8.2 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=refs%2Fheads%2Fdealii-8.2;p=dealii.git Merge pull request #457 from tamiko/dealii-8.2 Cherry-pick commits to the release branch --- 7d7f0ebcc5e5956eb09d180f5337207472b09efa