Add workflow_dispatch to makefile.yml

This should enable the use of manual triggers from GitHub UI.
leanprover · Feb 9, 2024 · c3a701b · c3a701b
1 parent 88b16da
commit c3a701b
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/.github/workflows/makefile.yml b/.github/workflows/makefile.yml
@@ -1,10 +1,13 @@
 name: Makefile CI
 
 on:
-  push:
-    branches: [ "main" ]
-  pull_request:
-    branches: [ "main" ]
+  # Run using manual triggers from GitHub UI:
+  # https://docs.github.com/en/actions/managing-workflow-runs/manually-running-a-workflow
+  workflow_dispatch: {}
+  # Run on pushes:
+  push: {}
+  # Run on every pull request:
+  pull_request: {}
 
 jobs:
   build: