Re: [PATCH] ci: avoid unnecessary builds

> On 11/3/22 9:34 AM, Johannes Schindelin via GitGitGadget wrote:
> > From: Johannes Schindelin <johannes.schindelin@gmx.de>
> >
> > Whenever a branch is pushed to a repository which has GitHub Actions
> > enabled, a bunch of new workflow runs are started.
> >
> > We sometimes see contributors push multiple branch updates in rapid
> > succession, which in conjunction with the impressive time swallowed by
> > even just a single CI build frequently leads to many queued-up runs.
> >
> > This is particularly problematic in the case of Pull Requests where a
> > single contributor can easily (inadvertently) prevent timely builds for
> > other contributors.
>
> As someone who is both the cause and the victim of this, I
> thank you for finding a way to reduce wasted CPU time. This
> patch looks good to me, though I'll need to trust the docs
> and your testing to be sure it will work. We will definitely
> see it in place as it merges into 'next' and 'main'.