From: Matthias Maier Date: Mon, 3 Jul 2023 04:05:17 +0000 (+0000) Subject: Merge pull request #15607 from tjhei/github-ci-disable-branch X-Git-Tag: relicensing~796 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=1934650b3f6bbf49a8c186220e2d9df2d3ef89e0;p=dealii.git Merge pull request #15607 from tjhei/github-ci-disable-branch disable github CI build of branches --- 1934650b3f6bbf49a8c186220e2d9df2d3ef89e0