Re: [PATCH v2] ci: cancel stale pull request workflow runs

[Junio C Hamano <gitster@pobox.com>]

Harald Nordgren <haraldnordgren@gmail.com> writes:

>> If a user has CI enabled on their own repository, pushes a commit
>> there, and opens a pull request, wouldn't GitHub Actions trigger
>> two events for the same commit at the tip of the pushed branch?
>>
>> Before this change, both events are assigned to the same concurrency
>> group (the commit object name).  One waits while the other runs, and
>> the skip-if-redundant logic stops the second one early without
>> wasting cycles on the same commit.  With this change, the
>> concurrency groups for these two events are separate.  Would we end
>> up building and testing the same commit twice in parallel?
>>
>> I suspect this may not be a problem in practice given how our
>> contributors use GitHub Actions in our official repositories (either
>> those owned by gitgitgadget or git).  They push to their own
>> repositories where CI may not be enabled, so 'push' does not
>> trigger.  Still, I thought it better to bring this up before the
>> change gets merged and wastes build cycles.
>
> Concurrency groups don't span repos, so I don't see a solution to that.

OK, then I do not see a need for solution to begin with---it is not
a problem, in other words ;-).

Thanks.