From: Daniel Arndt Date: Sat, 10 Sep 2016 22:13:44 +0000 (+0200) Subject: Merge pull request #3095 from bangerth/avoid-warning X-Git-Tag: v8.5.0-rc1~685 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9e7fc5ddb114c264e6c28b7f2078868ec16de16f;p=dealii.git Merge pull request #3095 from bangerth/avoid-warning Avoid a warning about an unused argument. --- 9e7fc5ddb114c264e6c28b7f2078868ec16de16f