From: Peter Munch <peterrmuench@gmail.com>
Date: Sun, 12 Mar 2023 12:13:53 +0000 (+0100)
Subject: Merge pull request #14876 from bangerth/message
X-Git-Tag: v9.5.0-rc1~497
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=8d39c9f4627a7a02cc17bd0a98187fee0e1de720;p=dealii.git

Merge pull request #14876 from bangerth/message

Minor improvement to an error message.
---

8d39c9f4627a7a02cc17bd0a98187fee0e1de720