Skip to content

Allow manual docs deploy dispatch#1591

Merged
MaxGhenis merged 1 commit intomainfrom
fix-workflow-triggers
Apr 15, 2026
Merged

Allow manual docs deploy dispatch#1591
MaxGhenis merged 1 commit intomainfrom
fix-workflow-triggers

Conversation

@MaxGhenis
Copy link
Copy Markdown
Collaborator

@MaxGhenis MaxGhenis commented Apr 15, 2026

Summary

  • add workflow_dispatch to the docs deploy workflow
  • make the GitHub Pages deploy recoverable when GitHub misses a main push trigger

Context

The #1590 merge commit reached main, but GitHub never emitted a PushEvent for that merge, so no push-triggered workflows were created for it. This does not fix GitHub missing a push event, but it gives us a clean manual recovery path for the docs deploy workflow without requiring another merge.

I checked the current versioning workflow on main before opening this PR. The stale changelog_entry.yaml path issue had already been fixed there, so this PR stays narrowly scoped to deploy recovery.

@MaxGhenis MaxGhenis merged commit 77f1f4c into main Apr 15, 2026
3 checks passed
@MaxGhenis MaxGhenis deleted the fix-workflow-triggers branch April 15, 2026 03:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant