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

Johannes Schindelin [off-list ref] 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.