From 70c400d20d477e728cbd887c41aa53a51285d05d Mon Sep 17 00:00:00 2001
From: patrick96
Date: Sun, 5 Nov 2023 20:02:24 +0100
Subject: [PATCH] doc: Specify boxes to check in GitHub release tool
---
doc/dev/release-workflow.rst | 3 +++
1 file changed, 3 insertions(+)
diff --git a/doc/dev/release-workflow.rst b/doc/dev/release-workflow.rst
index 3b66ff3b..0292391d 100644
--- a/doc/dev/release-workflow.rst
+++ b/doc/dev/release-workflow.rst
@@ -209,6 +209,9 @@ In addition using GitHub's "Auto-generate release notes" feature, the list of
new contributors should be generated and put at the end of the release notes.
The generated list of PRs can be removed.
+At the bottom, check the two boxes "Set as the latest release" and "Create a
+discussion for this release" (select the category "Announcements").
+
After-Release Checklist
~~~~~~~~~~~~~~~~~~~~~~~