Trigger deploy on master push

leanprover · Sep 6, 2023 · 84e4163 · 84e4163
1 parent d791f0a
commit 84e4163
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
@@ -1,9 +1,10 @@
 name: mdbook deploy to github pages
 
-# Controls when the action will run: only on manual dispatch from github UI
-on: workflow_dispatch
+on:
+  push:
+    branches:
+      - master
 
-# A workflow run is made up of one or more jobs that can run sequentially or in parallel
 jobs:
   Build:
     runs-on: ubuntu-latest