From: Denis Davydov <davydden@gmail.com>
Date: Fri, 11 May 2018 17:30:56 +0000 (+0200)
Subject: Merge pull request #6580 from tamiko/pr_6567
X-Git-Tag: v9.0.0~1
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=a8263760f3e98580cc7575a7663f1cc0981130ed;p=dealii.git

Merge pull request #6580 from tamiko/pr_6567

[9.0] take over #6567
---

a8263760f3e98580cc7575a7663f1cc0981130ed