From: Martin Kronbichler Date: Thu, 27 Mar 2025 20:16:46 +0000 (+0100) Subject: Merge pull request #18295 from marcfehling/github-names X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=725c4a00d35a82bd1bba4c2329e191dcb8e9e9f3;p=dealii.git Merge pull request #18295 from marcfehling/github-names github-actions: Simplify redundant names. --- 725c4a00d35a82bd1bba4c2329e191dcb8e9e9f3