Skip to content

chore: rename the Pages build job to build-site to avoid the required-status name#1170

Merged
kim-em merged 1 commit into
mainfrom
fix-pages-build-job-name
Jul 24, 2026
Merged

chore: rename the Pages build job to build-site to avoid the required-status name#1170
kim-em merged 1 commit into
mainfrom
fix-pages-build-job-name

Conversation

@kim-em

@kim-em kim-em commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

This PR renames the Pages workflow's build job to build-site (updating deploy's needs) so no job named build remains anywhere in the repo. A job named build auto-creates a check-run named build, which collides with the required build commit status context, the same collision #1156 fixed in pr-build.yml. Pages runs only on push-to-main and the daily schedule, never on a PR, so its check-run cannot wedge a PR today; this is hygiene so a future PR trigger here could never reintroduce the collision.

Note this touches .github/ so the scope check reports it out of scope and it needs a human merge; that is expected for a workflow change.

🤖 Prepared with Claude Code

…ired-status name

Rename jobs.build to jobs.build-site in pages.yml (updating deploy's `needs`)
so no job named `build` remains anywhere: a job named `build` auto-creates a
check-run named `build`, which collides with the required `build` commit
status context (the collision #1156 fixed in pr-build.yml). Pages runs only on
push-to-main / schedule, never on a PR, so its check-run cannot wedge a PR
today; this is hygiene so a future PR trigger here could never reintroduce the
collision.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019DP6TTvRPMYA6SPiA3Ff4u
@kim-em
kim-em requested a review from a team as a code owner July 24, 2026 23:17
@tauceti-review-bot tauceti-review-bot Bot added roadmap/none PR advances no roadmap (infra, refactor, or a Mathlib bump) awaiting-CI CI has not yet reported on the latest commit awaiting-review CI is green; waiting for review verdicts and removed awaiting-CI CI has not yet reported on the latest commit labels Jul 24, 2026
@kim-em
kim-em merged commit a1d89a0 into main Jul 24, 2026
9 of 10 checks passed
@kim-em
kim-em deleted the fix-pages-build-job-name branch July 24, 2026 23:21
@tauceti-review-bot tauceti-review-bot Bot removed the awaiting-review CI is green; waiting for review verdicts label Jul 24, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

roadmap/none PR advances no roadmap (infra, refactor, or a Mathlib bump)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant