From: Matthias Maier Date: Wed, 18 Dec 2024 19:18:19 +0000 (+0000) Subject: Merge pull request #17933 from bangerth/insert X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c39e5c3700f8fba9e89ecba5163e83667ef572da;p=dealii.git Merge pull request #17933 from bangerth/insert Just include a file directly. --- c39e5c3700f8fba9e89ecba5163e83667ef572da