diff options
| author | Silvan Mosberger <github@infinisil.com> | 2024-05-23 16:28:45 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-05-23 16:28:45 +0200 |
| commit | 0efcb15b4e7691dfe80e07f611cc13c365899579 (patch) | |
| tree | 2da06f5e7dc05ade88fd046a956662fa0561675a /.github | |
| parent | 5878d1d72f6da14590d99856bb04e024da536481 (diff) | |
| parent | d87803b7428dd56ef7f120c2ee853728ef812eaa (diff) | |
Merge pull request #313345 from katexochen/workflows/remove-check-by-name-concurrency
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/check-by-name.yml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/.github/workflows/check-by-name.yml b/.github/workflows/check-by-name.yml index e857c88f746d..ce7802f4aa8e 100644 --- a/.github/workflows/check-by-name.yml +++ b/.github/workflows/check-by-name.yml @@ -14,16 +14,16 @@ on: # While `edited` is also triggered when the PR title/body is changed, # this PR action is fairly quick, and PR's don't get edited that often, # so it shouldn't be a problem + # There is a feature request for adding a `base_changed` event: + # https://github.com/orgs/community/discussions/35058 types: [opened, synchronize, reopened, edited] permissions: {} -# Create a check-by-name concurrency group based on the pull request number. if -# an event triggers a run on the same PR while a previous run is still in -# progress, the previous run will be canceled and the new one will start. -concurrency: - group: check-by-name-${{ github.event.pull_request.number }} - cancel-in-progress: true +# We don't use a concurrency group here, because the action is triggered quite often (due to the PR edit +# trigger), and contributers would get notified on any canceled run. +# There is a feature request for supressing notifications on concurrency-canceled runs: +# https://github.com/orgs/community/discussions/13015 jobs: check: |