diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md
index 7680d0c10a..608528340d 100644
--- a/doc/dev/release_checklist.md
+++ b/doc/dev/release_checklist.md
@@ -13,7 +13,8 @@ We'll use `v4.6.0` as the intended release version as a running example.
 - In `src/CMakeLists.txt`, verify you see
   - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
   - `set(LEAN_VERSION_IS_RELEASE 1)`
-  - (both of these should already be in place from the release candidates)
+  - (all of these should already be in place from the release candidates)
+
 - `git tag v4.6.0`
 - `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
 - Now wait, while CI runs.
@@ -80,6 +81,11 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - There is no `stable` branch; skip this step
+    - [Reference Manual](https://github.com/leanprover/reference-manual)
+      - Dependencies: Verso
+      - Toolchain bump PR including updated Lake manifest
+      - Pushing the tag (whether for an RC or a final) triggers a deployment.
+      - There is no `stable` branch; skip this step
     - [Cli](https://github.com/leanprover/lean4-cli)
       - No dependencies
       - Toolchain bump PR
@@ -169,6 +175,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
 - `git tag v4.7.0-rc1`
 - `git push origin v4.7.0-rc1`
 - Now wait, while CI runs.
+  - The CI setup parses the tag to discover the `-rc1` special description, and passes it to `cmake` using a `-D` option. The `-rc1` doesn't need to be placed in the configuration file.
   - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
   - This step can take up to an hour.
 - (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d7fd855365..34564e72a1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -20,6 +20,11 @@ if (LEAN_SPECIAL_VERSION_DESC)
 elseif (NOT LEAN_VERSION_IS_RELEASE)
   string(APPEND LEAN_VERSION_STRING "-pre")
 endif()
+if (LEAN_VERSION_IS_RELEASE)
+  set(LEAN_MANUAL_ROOT "https://lean-lang.org/doc/reference/${LEAN_VERSION_STRING}/")
+else()
+  set(LEAN_MANUAL_ROOT "")
+endif()
 
 set(LEAN_PLATFORM_TARGET "" CACHE STRING "LLVM triple of the target platform")
 if (NOT LEAN_PLATFORM_TARGET)
diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean
index 53b5015016..e30026cf7b 100644
--- a/src/Lean/DocString/Links.lean
+++ b/src/Lean/DocString/Links.lean
@@ -11,11 +11,8 @@ set_option linter.missingDocs true
 
 namespace Lean
 
-/- After a stage0 update:
-@[extern "lean_get_manual_root"]
+@[extern "lean_manual_get_root"]
 private opaque getManualRoot : Unit → String
--/
-private def getManualRoot : Unit → String := fun () => ""
 
 private def fallbackManualRoot := "https://lean-lang.org/doc/reference/latest/"