Browse Source

Use Github's native concurrency control. (#12077)

Zeta 4 months ago
parent
commit
aa26d013c5

+ 0 - 14
.github/workflows/cancel.yml

@@ -1,14 +0,0 @@
-name: Cancel previous jobs
-on:
-  workflow_run:
-    workflows: ["CI"]
-    types:
-      - requested
-jobs:
-  cancel:
-    runs-on: ubuntu-latest
-    steps:
-    - name: Cancel previous runs
-      uses: styfle/[email protected]
-      with:
-        workflow_id: ${{ github.event.workflow.id }}

+ 4 - 0
.github/workflows/main.yml

@@ -7,6 +7,10 @@ on: [push, pull_request]
 env:
   OCAML_VERSION: 5.3.0
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   windows64-build:
     runs-on: windows-latest

+ 4 - 0
extra/github-actions/workflows/main.yml

@@ -6,6 +6,10 @@ on: [push, pull_request]
 env:
   OCAML_VERSION: 5.3.0
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   windows64-build:
     runs-on: windows-latest