From: Peter Munch <peterrmuench@gmail.com>
Date: Sat, 18 Mar 2023 08:14:32 +0000 (+0100)
Subject: Merge pull request #14911 from bangerth/grammar
X-Git-Tag: v9.5.0-rc1~464
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=a654d1fe45cc11c9dbbbcaaef6f53320f459baa2;p=dealii.git

Merge pull request #14911 from bangerth/grammar

Fix a grammar mistake.
---

a654d1fe45cc11c9dbbbcaaef6f53320f459baa2