Fix the docs deploy that silently stopped publishing

[bvdmitri]

The site is stale, not broken

Yesterday's fix (#99, 7f0219c) was correct and is in main. It just never shipped.

gh-pages is still on 6a5ca87 2026-08-25 build based on 8f843b7 — two days and several merges behind. So examples.rxinfer.com is still serving the pre-fix build, complete with the DocumenterMermaid <script type="module"> that caused the original outage. That is why math and highlighting still break there, and why it comes and goes between reloads: require.js attributes mermaid's anonymous define() to whichever module happens to be in flight, so the victim is jQuery on one load, katex-auto-render on the next, a mermaid chunk on the one after (Se.default.extend is not a function), and nobody on the one after that.

Verified with headless Chromium against the live URL — .katex element count flips between 14 and 0 across identical loads.

Why CI went green while publishing nothing

From the Documentation job of the last successful run (32966705464):

┌ Info: Deployment criteria for deploying devbranch build from GitHub Actions:
│ - ✘ ENV["DOCUMENTER_KEY"] or ENV["GITHUB_TOKEN"] exists and is non-empty
└ Deploying: ✘

360c14d added the "Check the built site renders" step and, in doing so, moved the env: block carrying GITHUB_TOKEN off the step that runs make docs onto the new one. deploydocs runs inside make docs. With no credentials Documenter decides this is not a deploy build, logs Deploying: ✘, and returns normally — the job stays green.

Changes

1. .github/workflows/CI.yml — credentials back on "Build documentation", where deploydocs actually runs. The render check needs neither the token nor the FastCholesky flag.

2. docs/make.jl — on refs/heads/main or a tag, error out when neither DOCUMENTER_KEY nor GITHUB_TOKEN is set, instead of finishing green having published nothing. PR builds (refs/pull/N/merge) are unaffected, so forks keep working.

3. docs/make.jl — strip Documenter's versions.js script tag from the built HTML. It is emitted relative to the site root assuming a versioned deployment; we deploy unversioned at the domain root (versions=nothing), so from /categories/basic_examples/x/ it resolves to ../../../../versions.js, above the root, and 404s on every page load. The version selector is already hidden without it. This was the first line in the console on every page — noise that hides real errors.

4. docs/src/how_build_works.md — a Deployment section documenting the silent-deploy hazard.

Verification

$ make docs && make docs-check
[ Info: Removed the unversioned-deploy `versions.js` script tag from 50 page(s)
OK    check-rendered-math: 782 formulas across 51 pages typeset cleanly (KaTeX 0.16.8).
OK    check-rendered-pages: 47 page(s) rendered math and highlighting correctly in Chromium.

$ grep -rl 'versions\.js' docs/build          # only comments in Documenter's own JS
$ grep -rl mermaid docs/build                 # empty

$ CI=true GITHUB_REF=refs/heads/main GITHUB_TOKEN= DOCUMENTER_KEY= julia --project=docs docs/make.jl
ERROR: LoadError: Refusing to finish a green build that would publish nothing.

$ CI=true GITHUB_REF=refs/pull/1/merge GITHUB_TOKEN= DOCUMENTER_KEY= julia --project=docs docs/make.jl
EXIT=0

After merge, confirm git ls-remote origin gh-pages advances and the live page no longer contains type="module".

🤖 Generated with Claude Code