From: Matthias Maier Date: Fri, 9 Feb 2024 17:48:18 +0000 (+0000) Subject: Merge pull request #16612 from tjhei/strip-comments-build-dir X-Git-Tag: relicensing~58 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=76b62594319f20cdcb84791ca063349486963ab1;p=dealii.git Merge pull request #16612 from tjhei/strip-comments-build-dir fix strip_comments target --- 76b62594319f20cdcb84791ca063349486963ab1