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

From: Junio C Hamano <gitster@pobox.com>
Date: Aug 21, 2023, 16:17 UTC
Message-ID: <xmqqttssqsj5.fsf@gitster.g>
In-Reply-To: <15b89f2e-adb8-ea2b-fd74-2cbe95e20501@gmx.de>

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

Show 15 quoted lines

> 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.