idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity

[ ci ] only run latest job

Browse Source 
As discussed on discord a while ago, this kills runs when a new
commit lands on the same branch. It should save some CI ressources.
This commit is contained in:
Guillaume Allais 2022-12-09 11:39:54 +00:00 committed by G. Allais
parent caeb55b495
commit 1d73e359e0
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.github/workflows/ci-idris2.yml vendored
View File

@ -32,6 +32,10 @@ on:
- '.github/workflows/ci-sphinx.yml'
- '.github/workflows/ci-super-linter.yml'
concurrency:
group: ${{ github.ref }}
cancel-in-progress: true
env:
IDRIS2_VERSION: 0.6.0 # For previous-version build