From: Denis Davydov Date: Fri, 6 Apr 2018 03:34:17 +0000 (+0200) Subject: Merge pull request #6173 from bangerth/fix-6161 X-Git-Tag: v9.0.0-rc1~223 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c120f879ecc8809ee27725c7fb6d5d3b3ab5f2ea;p=dealii.git Merge pull request #6173 from bangerth/fix-6161 Fix a couple minor issues with #6161. --- c120f879ecc8809ee27725c7fb6d5d3b3ab5f2ea