From: Bruno Turcksin Date: Mon, 8 May 2017 18:11:32 +0000 (-0400) Subject: Merge pull request #4357 from bangerth/minor-cleanups X-Git-Tag: v9.0.0-rc1~1614 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=5495c7bf9403a126050fbb729a5ba330231e370f;p=dealii.git Merge pull request #4357 from bangerth/minor-cleanups Some text cleanups. --- 5495c7bf9403a126050fbb729a5ba330231e370f