From: David Wells Date: Fri, 7 Feb 2025 22:17:28 +0000 (-0500) Subject: Merge pull request #18100 from bangerth/empty-2 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ae2745de1b7d7c7c9268e5eccf01a8d1ad461a29;p=dealii.git Merge pull request #18100 from bangerth/empty-2 Remove an unnecessary include path. --- ae2745de1b7d7c7c9268e5eccf01a8d1ad461a29