Re: main != master at github.com/git/git

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

Johannes Schindelin <Johannes.Schindelin@gmx.de> writes:

> My understanding is that the recommended way to handle this via the
> `concurrency` key [*1*]. That is, if we changed
>
>     concurrency:
>       group: windows-build-${{ github.ref }}
>       cancel-in-progress: ${{ needs.ci-config.outputs.skip_concurrent == 'yes' }}
>
> to
>
>     concurrency:
>       group: windows-build-${{ github.sha }}
>
> then pushing both `master` and `next` pointing at the same commit would
> start only one of the workflow runs immediately, keeping the second one
> pending until the first run is done.

Perfect.  It is much better than pushing 'master@{24.hours.ago} to
'main' which was what I used to do avoid the problem between these
two, which I stopped doing because it did not work well.

> If the first run succeeds, the second
> run will pick up that status and avoid running everything all over again,
> via `skip-if-redundant`.

Nice.  I understand that this would kick in regardless, but the
right use of the concurrency key would make it far more effective.

Very nice.