From: Matthias Maier Date: Mon, 5 May 2025 18:23:48 +0000 (+0000) Subject: Merge pull request #18336 from bangerth/header-configuration X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=89691efb79bd689aadd5e952313a6ac840bab11e;p=dealii.git Merge pull request #18336 from bangerth/header-configuration Push configuration of header subdirectories down to these subdirectories. --- 89691efb79bd689aadd5e952313a6ac840bab11e