-
-
Notifications
You must be signed in to change notification settings - Fork 2.9k
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
ci: tear down docs infra after PR is merged & release fixes #9893
Conversation
2ed0407
to
c861f19
Compare
80152aa
to
83477a5
Compare
83477a5
to
95e818a
Compare
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.
Would it be better to proxy this through another workflow?
- name: Comment | ||
uses: actions-cool/maintain-one-comment@v3 | ||
with: | ||
number: ${{ github.event.number }} | ||
delete: true | ||
body-include: '<!-- Docs PR URL -->' |
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.
Thoughts on instead editing the comment to say something about the preview deployment being removed? Might also be nice as a bit of feedback on whether this workflow broke or such.
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.
"🧹 Cleaned up docs preview"
No description provided.