From: Marc Fehling 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