Skip to content

Commit 598b3ae

Browse files
committed
Add manual trigger support to GitHub Actions
- Add workflow_dispatch trigger for manual documentation deployment - Allow deploy-docs job to run on manual trigger - This enables redeployment of subdirectory docs when they get overwritten
1 parent 5235494 commit 598b3ae

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

.github/workflows/CI.yml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ on:
66
tags:
77
- '*'
88
pull_request:
9+
workflow_dispatch: # Manual trigger for documentation deployment
910
concurrency:
1011
# Skip intermediate builds: always.
1112
# Cancel intermediate builds: only if it is a pull request build.
@@ -41,8 +42,8 @@ jobs:
4142
name: Deploy Documentation
4243
runs-on: ubuntu-latest
4344
needs: test
44-
# Only deploy on push to main (not on PRs)
45-
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
45+
# Only deploy on push to main (not on PRs) OR manual trigger
46+
if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch'
4647
steps:
4748
- uses: actions/checkout@v4
4849
- uses: julia-actions/setup-julia@v1

0 commit comments

Comments
 (0)