From: Matthias Maier Date: Sun, 4 May 2025 02:02:14 +0000 (+0000) Subject: Merge pull request #18410 from bangerth/precise X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=8b194d9ddf1dc0a7645c4f8160f99679f6f16d92;p=dealii.git Merge pull request #18410 from bangerth/precise Be more precise with which files we compile. --- 8b194d9ddf1dc0a7645c4f8160f99679f6f16d92