From: Martin Kronbichler Date: Fri, 24 Jul 2015 16:30:02 +0000 (+0200) Subject: Merge pull request #1188 from bangerth/fix-comments X-Git-Tag: v8.4.0-rc2~727 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=6b8faa1fb48375219f3f6305c14f758ff13147e7;p=dealii.git Merge pull request #1188 from bangerth/fix-comments A couple of forgotten things. --- 6b8faa1fb48375219f3f6305c14f758ff13147e7