From 46a0a0eb59f9f3637b4a8c5ea4dc25932a154167 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 1 Apr 2026 16:01:00 +1100 Subject: [PATCH] chore: add safety notes to release command (#13225) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds two safety notes to the Claude Code release command: - Mathlib bump branches live on `mathlib4-nightly-testing`, not the main `mathlib4` repo - Never force-update remote refs without explicit user confirmation 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 (1M context) --- .claude/commands/release.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/.claude/commands/release.md b/.claude/commands/release.md index 06e7dfd06a..b2fbdbb178 100644 --- a/.claude/commands/release.md +++ b/.claude/commands/release.md @@ -157,6 +157,16 @@ Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail) fail while others are still running, `--watch` will continue until everything settles, then exit with a non-zero code. So a background `--watch` finishing = all checks done; check which failed. +## Mathlib Bump Branches + +Mathlib `bump/v4.X.0` branches live on the **fork** `leanprover-community/mathlib4-nightly-testing`, +NOT on `leanprover-community/mathlib4`. + +## Never Force-Update Remote Refs Without Confirmation + +Never force-update an existing remote branch or tag via `git push --force` or the GitHub API +without explicit user confirmation. + ## Error Handling **CRITICAL**: If something goes wrong or a command fails: