From: Matthias Maier Date: Mon, 7 Apr 2025 16:16:03 +0000 (+0000) Subject: Merge pull request #18335 from bangerth/remove-comment X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9c4075ddf49b2c7374ae98766467eb5364fafdef;p=dealii.git Merge pull request #18335 from bangerth/remove-comment Remove a comment that is no longer accurate. --- 9c4075ddf49b2c7374ae98766467eb5364fafdef