From: Timo Heister <timo.heister@gmail.com>
Date: Wed, 30 Oct 2024 19:54:28 +0000 (-0400)
Subject: Merge pull request #17818 from bangerth/doc
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d703fda1ad73dc37b9af859b30aaf3ee5f452061;p=dealii.git

Merge pull request #17818 from bangerth/doc

Fix terminology.
---

d703fda1ad73dc37b9af859b30aaf3ee5f452061