chore: only run push CI jobs on pushes to main

Reduce wasted CI work!
leanprover · Sep 4, 2024 · b9471f0 · b9471f0
1 parent 979a578
commit b9471f0
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -1,5 +1,7 @@
 on:
   push:
+    branches:
+      - main
   pull_request:
 
 name: CI