ci(docs): restore the 'run documentation' label gate

[ocots]

Why

#875 removed the run documentation label gate and replaced it with an automatic paths
trigger. The premise was that the label had never been applied to any of the twelve
documentation pull requests, and that this was an oversight.

It was not an oversight — the label is the mechanism. It exists so documentation builds are
started deliberately instead of on every push, and the rewrite was verified locally with the
intent of finalising the docs before running builds online. #875 removed a control that was
working as designed.

What changes

.github/workflows/Documentation.yml goes back to its pre-#875 state, byte for byte. The
paths filter goes away with the rest: once a human decides when the job runs, a path filter
decides nothing.

The restored condition is worth restating, because it is more carefully built than it looks:

if: >
  github.event_name != 'pull_request' ||
  (github.event.action == 'labeled' && github.event.label.name == 'run documentation') ||
  (github.event.action != 'labeled' && contains(github.event.pull_request.labels.*.name, 'run documentation'))

• On a labeled event it reacts only to run documentation — otherwise adding three labels
  in a row would start three builds.
• On opened / synchronize / reopened it checks that the PR currently carries the label.
  So a build is opted into once, and then repeats on every push for as long as the label stays.

This also puts the repository back in line with the Handbook's Documentation.yml template
(VITEPRESS-DOC.md:484-493), which #875 had made OptimalControl the only package to diverge
from.

What is kept

docs/src/index.md keeps the Draft = false that #875 added. It is independent of the trigger,
and without it the landing page's five @example blocks execute nowhere — not in CI, not
locally. That one was a real gap.

Verification

This PR touches only the workflow. For a pull_request event GitHub evaluates the workflow file
from the PR head, so the restored file governs this PR too: no Documentation job should start
here unless the run documentation label is added. That is the check.

🤖 Generated with Claude Code