| ... | @@ -7,8 +7,10 @@ on: | ... | @@ -7,8 +7,10 @@ on: |
| 7 | - master | 7 | - master |
| 8 | workflow_dispatch: | 8 | workflow_dispatch: |
| 9 | | 9 | |
| | 10 | # This cancels older workflow runs on pull requests while ensuring that there |
| | 11 | # are no concurrency limits on pushes and manual workflow dispatches. |
| 10 | concurrency: | 12 | concurrency: |
| 11 | group: ${{ github.head_ref || github.run_id }}-${{ github.actor }} | 13 | group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.run_id }} |
| 12 | cancel-in-progress: ${{ github.event_name == 'pull_request' }} | 14 | cancel-in-progress: ${{ github.event_name == 'pull_request' }} |
| 13 | | 15 | |
| 14 | permissions: | 16 | permissions: |