As soon as nightly-testing is up-to-date with 2025-12-02, which includes https://github.com/leanprover/lean4/pull/7965, I should document the new behavior.