From 8821830984b0c0f32d177ba3d3bb0a1d26037e4f Mon Sep 17 00:00:00 2001 From: Peter Corke Date: Sat, 29 Aug 2026 07:48:13 +0200 Subject: [PATCH] ci: let workflow_dispatch actually deploy docs, rename to "Docs Publish" docs.yml already had a workflow_dispatch trigger, but the Pages-artifact upload and the deploy job were both gated on github.event_name == 'push', so a manual run silently built the docs and threw the result away without publishing anything. Widens both to also allow workflow_dispatch, and adds an explicit ref check on deploy (dispatch can target any branch, push is already restricted to main via the branches: filter). Also renames the workflow to "Docs Publish" to match the same button across RTB/MVTB/bdsim. --- .github/workflows/docs.yml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 4b72887c..b81ff65f 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -1,4 +1,4 @@ -name: Docs +name: Docs Publish on: push: @@ -173,15 +173,21 @@ jobs: path: docs/build/html/mvtb_notebooks.zip if-no-files-found: error + # push and workflow_dispatch both publish; pull_request only builds + # (to catch breakage in review), it never gets an artifact to deploy. - uses: actions/upload-pages-artifact@v5 - if: github.event_name == 'push' + if: github.event_name == 'push' || github.event_name == 'workflow_dispatch' with: path: docs/build/html deploy: needs: build runs-on: ubuntu-latest - if: github.event_name == 'push' + # ref check (not just event_name) so a manual dispatch from a + # non-main branch builds but doesn't publish -- push is already + # restricted to main via the `branches: [main]` filter above, but + # workflow_dispatch can be run against any branch. + if: (github.event_name == 'push' || github.event_name == 'workflow_dispatch') && github.ref == 'refs/heads/main' environment: name: github-pages url: ${{ steps.deployment.outputs.page_url }}