Update Makefile CI to run on all pull request activity

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