From: Bruno Turcksin <bruno.turcksin@gmail.com>
Date: Thu, 23 Jul 2015 22:58:51 +0000 (-0500)
Subject: Merge pull request #1181 from bangerth/remove-unused-variable
X-Git-Tag: v8.4.0-rc2~730
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=4b72966a7ec681c7d5cd31805695666d6dcacf64;p=dealii.git

Merge pull request #1181 from bangerth/remove-unused-variable

Remove an unused variable.
---

4b72966a7ec681c7d5cd31805695666d6dcacf64