Skip to content

chore: drop the GitHub Pages jobs from the release workflow - #33

Merged
davidpoblador merged 1 commit into
mainfrom
chore/drop-pages-jobs
Aug 21, 2026
Merged

davidpoblador merged 1 commit into
mainfrom
chore/drop-pages-jobs

Conversation

@davidpoblador

Copy link
Copy Markdown
Member

The docs are served from a Garage bucket now — DNS points at origin.alltuner.com, GitHub Pages is disabled on this repo, and publish-site.yml builds the same mkdocs site and attaches it for the fleet's publisher to place.

These two jobs would not merely be redundant, they would fail: actions/deploy-pages errors on a repo with Pages disabled, so the next release would go red.

Removes build-docs and deploy-docs, and the now-unused pages: write permission. Nothing else in the workflow referenced them — the script used refuses to remove a job another job still needs. Verified the result still parses and the remaining jobs are unchanged.

🤖 Generated with Claude Code

https://claude.ai/code/session_01UmbxWdLwrqjTqvw2ECuoEa

The docs are served from a Garage bucket now, and publish-site.yml builds the
same mkdocs site for the fleet's publisher to place. These jobs would not just
be redundant: deploy-pages errors on a repo with Pages disabled, so the next
release would fail on them.

Also drops the pages: write permission, which now grants nothing.
@davidpoblador
davidpoblador merged commit 0fba17c into main Aug 21, 2026
6 checks passed
@davidpoblador
davidpoblador deleted the chore/drop-pages-jobs branch August 21, 2026 13: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