From: Marc Fehling <mafehling.git@gmail.com>
Date: Tue, 20 Aug 2024 17:05:26 +0000 (-0600)
Subject: Merge pull request #17577 from bangerth/doc
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9d380e4f34f02a5d5116311315a8c0037c0f9780;p=dealii.git

Merge pull request #17577 from bangerth/doc

Leave a comment in the documentation.
---

9d380e4f34f02a5d5116311315a8c0037c0f9780