CI: Do not run multiple note-pushing workflow runs in parallel

In 1d03944a9c failures from pushing notes were ignored entirely due to
the command failing sporadically. Looking at the original commit message
this was almost certainly due to the fact that multiple runs of the
workflow could happend simulaneously if PRs were merged in quick
succession:

1. PR 1 gets merged.
2. Workflow run 1 gets triggered for newly pushed `master` commit from
   PR 1 and fetches notes ref at `aaaaaaa`.
3. PR 2 gets merged.
4. Workflow run 2 gets triggered for newly pushed `master` commit from
   PR 2 and fetches notes ref at `aaaaaaa` as well.
5. Workflow run 1 finishes its work and pushes `bbbbbbb` to the notes
   ref.
6. Workflow run 2 finishes as well, tries to push `ccccccc` to the notes
   ref, but gets rejected. This is because its changes are based on
   `aaaaaaa` and cannot be fast-forwarded due to workflow run 1 having
   pushed different notes in the meantime.

This sequence of events could also be observed after bbad346add got
merged, which caused the first couple workflow runs after to be very
slow as they were processing a large backlog of missing notes.

Instead of silencing the error when it happens and relying on the fact
that the next run will correct it, let's just prevent the conflict from
happening in the first place by disallowing parallel runs of the
workflow. This avoids unnecessary workflow runs and allows detection of
other, unexpected errors happening when pushing.
This commit is contained in:
InvalidUsernameException
2026-02-07 16:56:30 +01:00
committed by Jelle Raaijmakers
parent 5f70d40feb
commit 0c5684f7ff
Notes: github-actions[bot] 2026-02-25 09:09:33 +00:00

View File

@@ -6,6 +6,9 @@ on:
permissions:
contents: write
concurrency:
group: ${{ github.workflow }}
jobs:
build:
if: github.repository == 'LadybirdBrowser/ladybird'
@@ -19,6 +22,6 @@ jobs:
git fetch origin "refs/notes/*:refs/notes/*"
curl -fsSLO https://github.com/gh-tui-tools/git-gloss/raw/refs/heads/main/git-gloss
bash ./git-gloss
git push origin "refs/notes/*" || true
git push origin "refs/notes/*"
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}