Skip to content

docs: fix gh-pages races and fix manual dispatch for docs publish workflow#2420

Open
sespiros wants to merge 2 commits into
mainfrom
sse/docs-deploy-concurrency
Open

docs: fix gh-pages races and fix manual dispatch for docs publish workflow#2420
sespiros wants to merge 2 commits into
mainfrom
sse/docs-deploy-concurrency

Conversation

@sespiros
Copy link
Copy Markdown
Collaborator

No description provided.

@sespiros sespiros requested a review from charludo May 27, 2026 15:15
@sespiros sespiros added the no changelog PRs not listed in the release notes label May 27, 2026
@github-actions
Copy link
Copy Markdown

PR Preview Action v1.8.1

QR code for preview link

🚀 View preview at
https://edgelesssys.github.io/contrast/pr-preview/pr-2420/

Built to branch gh-pages at 2026-05-27 15:17 UTC.
Preview will be ready when the GitHub Pages deployment is complete.

(github.event_name == 'pull_request' && github.repository_owner == github.event.pull_request.head.repo.owner.login)
env:
PREVIEW: ${{ !(github.event_name == 'push' && github.ref_name == 'main') }}
PREVIEW: ${{ github.event_name == 'pull_request' }}
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this not mean a manual dispatch does a real publication? IMO that should not be possible unless we merge into main. What's the motivation behind the condition change?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. Yesterday I merged the update release PR and another docs change PR (to update the debugshell page). These triggered 2 gh-pages publish jobs which they raced and as a result the release to main docs got published but my changes to the debugshell docs didn't (you can visit the docs->next and check the debugshell page). The docs will be updated when some other update to main touches the docs but I don't see why couldn't we dispatch the workflow ourselves.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

no changelog PRs not listed in the release notes

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants