ci: split the docs job so only deploy holds contents: write

[tannevaled]

Last live exposure from the fleet-wide least-privilege Pages sweep. This repo is one of 18 whose docs.yml ran build and deploy in a single job, gated only at the step level with if: github.event_name != 'pull_request'.

Step gating decides which steps run. It does not change the token the job holds. So unlike the other 545 repos in the sweep -- where the concern was latent, because a job boundary already separated build from deploy -- here the pull request build genuinely ran holding contents: write.

The split

• build -- contents: read, runs on every event, proves mkdocs build --strict still passes.
• deploy -- holds contents: write alone, needs: build, gated on github.event_name != 'pull_request': the exact condition that used to sit on the "Configure git" step, lifted to the job. What publishes, and when, is unchanged.

The two mike deploy steps keep their own if: conditions verbatim, so the branch-vs-tag behaviour is untouched.

No artifact crosses between the jobs, and none needs to

mike deploy runs mkdocs build itself and commits its own output to gh-pages. The site/ that mkdocs build --strict produced was already thrown away before this split -- it was a validation build, never the published one. So the build job is the gate and the deploy job publishes, exactly the division of labour the single job had, now with a permission boundary between them.

The cost is that the site is built twice. That is deliberate: it is what keeps the published output byte-for-byte identical to what was published before.

Concurrency group on the deploy job

mike deploy writes the gh-pages branch over the network. This workflow triggers on both push: branches: [main] and push: tags: ["v*"], so publishing a release sends both a branch update and a tag update, starting two runs that race -- the loser failing outright with ! [rejected] gh-pages -> gh-pages (fetch first). cancel-in-progress stays false deliberately: making a publish wait is better than killing one part way through.

Verification

Nothing changed but the structure and the two permission keys -- asserted by parsing both files and comparing the step lists element by element, not by reading the diff. The published gh-pages tree is compared before and after by tree sha, so a split that silently stopped publishing, or published something different, shows up as a changed tree rather than as a green check.