From: Marc Fehling <mafehling.git@gmail.com>
Date: Fri, 29 Oct 2021 02:14:28 +0000 (-0600)
Subject: Merge pull request #12899 from bangerth/message
X-Git-Tag: v9.4.0-rc1~875
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=7df07c0ee2a08873a02455598acef15db2d87015;p=dealii.git

Merge pull request #12899 from bangerth/message

Improve an error message.
---

7df07c0ee2a08873a02455598acef15db2d87015