diff options
| author | Guillaume Boisseau | 2024-05-14 16:26:36 +0200 |
|---|---|---|
| committer | GitHub | 2024-05-14 16:26:36 +0200 |
| commit | d7390c53fba81768bfa08645e18dff4f613d7aa4 (patch) | |
| tree | f1f1c33876972f7ed2216f9ca532961213662a36 | |
| parent | 0d5ef8ac5abc49e5adabee97edbb7ff712bd8d10 (diff) | |
| parent | 63680b7bd578b4153606bd5b37fd6563c933eb0d (diff) | |
Merge pull request #180 from AeneasVerif/ci
ci: cancel jobs after force-push to a branch
Diffstat (limited to '')
| -rw-r--r-- | .github/workflows/ci.yml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index eeb423b6..56769cae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,6 +25,7 @@ jobs: with: concurrent_skipping: 'same_content_newer' skip_after_successful_duplicate: 'true' + cancel_others: 'true' outputs: should_skip: ${{ steps.skip_check.outputs.should_skip }} |