[Doc] A pull request without the preview label announces a deployment that never happens #410

Written by Claude (Claude Code) at the request of ocots.

Problem

On a pull request labelled run documentation but not documentation push preview, the documentation job announces a deployment that never happens. Log of #403 (run 42367055247):

DOCUMENTER_PUSH_PREVIEW: false
┌ Info: Deployment criteria for deploying preview build from GitHub Actions:
│ - ✔ `push_preview` keyword argument to deploydocs is `true`
└ Deploying: ✔
[ Info: Bases that will be built: ["previews/PR403"]
[ Info: Deploying docs for base "previews/PR403" from build/1
┌ Info: Deployment criteria for deploying preview build from GitHub Actions:
│ - ✘ `push_preview` keyword argument to deploydocs is `true`
└ Deploying: ✘

Cause

DocumenterVitepress.MarkdownVitepress decides where the site is deployed during makedocs. When make.jl gives it no deploy_decision, it computes one with push_preview=true hard-coded (DocumenterVitepress 0.3, src/writer.jl, render). The label, read through DOCUMENTER_PUSH_PREVIEW (set by CTActions), only reaches deploydocs. So the site is built for previews/PR<n>, the deployment is announced, and deploydocs then refuses it.

Fix

Take the decision once, with the label, in docs/make.jl:

• compute deploy_decision = Documenter.deploy_folder(Documenter.auto_detect_deploy_system(); repo, devbranch, devurl, push_preview) with push_preview read from DOCUMENTER_PUSH_PREVIEW;
• pass it to MarkdownVitepress(; deploy_decision);
• call DocumenterVitepress.deploydocs only when deploy_decision.all_ok (and bases.txt exists), and say why otherwise.

Without the label, the site is built at the root and the log says that no preview was requested. The template of SITE13 in ct-conventions is updated the same way.

Done when

• A pull request with run documentation and without documentation push preview builds without announcing a deployment, and says why it does not deploy.
• With documentation push preview, the preview is built for previews/PR<n> and deployed.
• A push to main still deploys dev.