CI: Run when a PR is opened

leanprover · Feb 14, 2024 · 8184ccf · 8184ccf
1 parent d3d2940
commit 8184ccf
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/.github/workflows/makefile.yml b/.github/workflows/makefile.yml
@@ -6,8 +6,10 @@ on:
   workflow_dispatch: {}
   # Run on every push:
   push: {}
-  # Run on every pull request:
-  pull_request: {}
+  # Run when a pull request has been opened:
+  pull_request: 
+    types:
+      - opened
 
 jobs:
   build: