From: Matthias Maier Date: Fri, 14 Aug 2015 02:44:05 +0000 (-0500) Subject: Merge pull request #1358 from bangerth/fix-broken-merge-1343 X-Git-Tag: v8.4.0-rc2~610 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ca6683625f765b021719618db0e79013f98be749;p=dealii.git Merge pull request #1358 from bangerth/fix-broken-merge-1343 Fix #1343. --- ca6683625f765b021719618db0e79013f98be749