From 443d119613b09cfa85fcadda6c11951749f454ef Mon Sep 17 00:00:00 2001 From: Max Horn Date: Fri, 7 Nov 2025 13:41:19 +0100 Subject: [PATCH] CI: Limit concurrency of Docu jobs When building tests on master, we normally let *all* of them complete not just the latest one, as that helps with pinpointing caused by merging PRs in parallel that then interact badly. But for the documentation job this is problematic: it can happen that we merge multiple PRs simultaneously, resulting in multiple concurrent CI jobs running on `master``. But the Docu job for the last merged PR may not be the last to finish. In that case, the job which actually finishes last "wins" and pushes its version of the documentation. As a result, the documentation does not reflect any changes from the last merged PRs (and possibly more). Even with the changes in this PR, there is still a problem when a PR CI job pushes a docs preview in concurrency to a CI job on master updating the docs. --- .github/workflows/Docu.yml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/.github/workflows/Docu.yml b/.github/workflows/Docu.yml index 0f09daa7b1a2..ec6073e0de23 100644 --- a/.github/workflows/Docu.yml +++ b/.github/workflows/Docu.yml @@ -18,11 +18,10 @@ on: workflow_dispatch: concurrency: - # group by workflow and ref; the last slightly strange component ensures that for pull - # requests, we limit to 1 concurrent job, but for the master branch we don't - group: ${{ github.workflow }}-${{ github.ref }}-${{ github.ref != 'refs/heads/master' || github.run_number }} - # Cancel intermediate builds, but only if it is a pull request build. - cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }} + # group by workflow and ref + group: ${{ github.workflow }}-${{ github.ref }} + # Cancel intermediate builds, only the latest on a given branch or PR should complete + cancel-in-progress: true jobs: deploy_docs: