From: Denis Davydov Date: Thu, 7 Jul 2016 21:46:14 +0000 (+0200) Subject: Merge pull request #2776 from bangerth/minor-cleanups X-Git-Tag: v8.5.0-rc1~909 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=691e74d0d801632f2ddacc29df708bbffc4ef7ca;p=dealii.git Merge pull request #2776 from bangerth/minor-cleanups Minor cleanups. --- 691e74d0d801632f2ddacc29df708bbffc4ef7ca