rm launch ci

rjbou · Jul 8, 2024 · 0d69f8c · 0d69f8c
1 parent cc0735f
commit 0d69f8c
Showing 1 changed file with 0 additions and 11 deletions.
diff --git a/.github/workflows/depexts.yml b/.github/workflows/depexts.yml
@@ -1,16 +1,5 @@
 name: depexts
 
-on:
-  pull_request:
-    paths:
-      - 'src/state/opamSysInteract.ml'
-      - '.github/workflows/depexts.yml'
-      - '.github/scripts/depexts/**'
-  push:
-    paths:
-      - 'master'
-      - 'gha-depexts'
-      - '2.**'
 
 defaults:
   run: