From: Junio C Hamano Date: Sun, 03 May 2020 16:46:15 GMT Subject: Re: [PATCH] ci: respect the [skip ci] convention in our GitHub workflow "CI/PR" Message-ID: In-Reply-To: <20200503093646.GC170902@coredump.intra.peff.net> Jeff King writes: > I'm not sure whether we want to be building all of the individual topics > in gitster/git or not. In theory that provides more information, but I'm > not sure if anybody is looking at them (and all of the notifications > would go to Junio anyway). I do not think I am letting GitHub notifications for gitster/* come to my mailbox, so it is quite possible that many have piled up there without anybody (not even me) seeing them. I won't be locally able to notice breakages introduced by an individual topic to an environment I do not have access to, and building these topics with GitHub Actions may reveal which ones break, say, vsbuild, but I won't be debugging and fixing such issues myself anyway, so at least to me it is useless to run build there. I think I agree with your outline, i.e. build pull requests to help contributors, and build public integration branches to help the project as a whole. Thanks.