From: Marc Fehling <mafehling.git@gmail.com>
Date: Wed, 26 Apr 2023 03:13:19 +0000 (-0600)
Subject: Merge pull request #15139 from bangerth/glossary
X-Git-Tag: v9.5.0-rc1~288
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=b4f1d161544a0d4e02372f6edbe8979ead33da2c;p=dealii.git

Merge pull request #15139 from bangerth/glossary

Add necessary include files to a code snippet in the glossary.
---

b4f1d161544a0d4e02372f6edbe8979ead33da2c