mirror of
https://github.com/storytold/winprint.rs.git
synced 2026-11-15 06:44:28 +00:00
ci: give runs outside pull requests their own concurrency group
This commit is contained in:
1 parent
0a6a76a0c4
commit
dc32aa7ad8
2 files changed
+6
-4
No files matched your search
@@ -9,8 +9,9 @@ on:
|
||||
permissions:
|
||||
contents: read
|
||||
concurrency:
|
||||
group: gdi-${{ github.ref }}
|
||||
# A newer push to a pull request replaces its older run; runs on main always finish.
|
||||
# Pull requests share one group per branch, so a newer push cancels the older run. Every other
|
||||
# run (main, manual) gets a group of its own, so it is neither cancelled nor replaced while queued.
|
||||
group: gdi-${{ github.event_name == 'pull_request' && github.ref || github.run_id }}
|
||||
cancel-in-progress: ${{ github.event_name == 'pull_request' }}
|
||||
jobs:
|
||||
gdi:
|
||||
|
||||
@@ -12,8 +12,9 @@ permissions:
|
||||
contents: read
|
||||
|
||||
concurrency:
|
||||
group: test-${{ github.ref }}
|
||||
# A newer push to a pull request replaces its older run; runs on main always finish.
|
||||
# Pull requests share one group per branch, so a newer push cancels the older run. Every other
|
||||
# run (main, manual) gets a group of its own, so it is neither cancelled nor replaced while queued.
|
||||
group: test-${{ github.event_name == 'pull_request' && github.ref || github.run_id }}
|
||||
cancel-in-progress: ${{ github.event_name == 'pull_request' }}
|
||||
|
||||
env:
|
||||
|
||||
Reference in new issue
Block a user