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

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.


Harald