From: Daniel Arndt Date: Thu, 3 Feb 2022 18:50:26 +0000 (-0500) Subject: Merge pull request #13331 from tjhei/remove_some_stray_comments X-Git-Tag: v9.4.0-rc1~535 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=8200160107bc92cfae24905f1cbbaf69569a3290;p=dealii.git Merge pull request #13331 from tjhei/remove_some_stray_comments --- 8200160107bc92cfae24905f1cbbaf69569a3290