-
Notifications
You must be signed in to change notification settings - Fork 27.4k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Docs: add the ability to manually trigger jobs #33598
Conversation
The docs for this PR live here. All of your documentation changes will be reflected on that endpoint. The docs are available until 30 days after the last update. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nice!
@@ -1,6 +1,7 @@ | |||
name: Build documentation | |||
|
|||
on: | |||
workflow_dispatch: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My only concern is if ${{ github.sha }}
(see below) will be the correct (previous) release tag commit.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
According to Github doc here: https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#workflow_dispatch
Last commit on the GITHUB_REF branch or tag
So I think it should work fine.
What does this PR do?
Our doc-builder had a bug that was fixed recently (huggingface/doc-builder#516). This bug has an impact on our docs since v4.41 -- we need to manually trigger the job to push the fixed docs.
This PR adds the ability to manually trigger the doc builder :)