From: Luca Heltai <luca.heltai@sissa.it>
Date: Mon, 7 Mar 2016 13:27:06 +0000 (+0100)
Subject: Merge pull request #2315 from bangerth/minor-cleanup3-5
X-Git-Tag: v8.5.0-rc1~1239
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=3e70c2897561fdb88b9f634f32fad0364dcebdf0;p=dealii.git

Merge pull request #2315 from bangerth/minor-cleanup3-5

Minor cleanups.
---

3e70c2897561fdb88b9f634f32fad0364dcebdf0