From 1e846f2e13a55e20f515811ded97d709236b95d0 Mon Sep 17 00:00:00 2001 From: Jiangki Date: Thu, 23 Jul 2026 15:47:47 +0000 Subject: [PATCH] ci: deploy docs site on pushes to main Keep workflow_dispatch for manual runs, and auto-deploy after main merges so GitHub Pages stays current without a separate click. --- .github/workflows/docs-deploy.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docs-deploy.yml b/.github/workflows/docs-deploy.yml index 2836fcb..825ad40 100644 --- a/.github/workflows/docs-deploy.yml +++ b/.github/workflows/docs-deploy.yml @@ -1,13 +1,14 @@ # Deploys the mdBook docs site to GitHub Pages. # -# DELIBERATELY manual-only (workflow_dispatch) so documentation deployments -# remain explicit. Add a `push: branches: [main]` trigger if continuous -# deployment becomes preferable. +# Deploys on every push to main (docs stay in sync with the default branch) +# and still allows manual runs via workflow_dispatch. # # Prerequisite: repository Settings -> Pages -> Source = "GitHub Actions". name: Deploy docs on: + push: + branches: [main] workflow_dispatch: permissions: