You've already forked library-registry
mirror of
https://github.com/arduino/library-registry.git
synced 2025-07-09 01:42:00 +03:00
Configure manager workflow to prevent parallel runs for one PR
It was previously possible to trigger the "Manage PRs" workflow for a pull request while a previous run for that PR is already in process. When that happens, it can result in erroneous bot comments. For example: 1. Workflow run is automatically triggered by a push. 2. Contributor does not notice this and comments a mention of the bot to trigger the workflow. 3. The first workflow run finds the PR is compliant and merges it. 4. The second workflow run finds the PR is compliant and attempts to merge it. 5. The second workflow run fails the merge (because it is already merged) and informs the contributor that there was a merge conflict they must resolve. 6. The contributor is not able to resolve the non-existent conflict and is left wondering whether their submission was successful. The solution is to configure the "Manage PRs" workflow so that a workflow run in progress is canceled if the workflow is triggered again for that PR. The "concurrency group" name is the PR number, so workflow runs in progress for other PRs would not be affected.
This commit is contained in:
4
.github/workflows/manage-prs.yml
vendored
4
.github/workflows/manage-prs.yml
vendored
@ -24,6 +24,10 @@ on:
|
||||
- created
|
||||
- edited
|
||||
|
||||
concurrency:
|
||||
group: ${{ github.event.pull_request.number }}${{ github.event.issue.number }}
|
||||
cancel-in-progress: true
|
||||
|
||||
jobs:
|
||||
diff:
|
||||
if: >
|
||||
|
Reference in New Issue
Block a user