max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add guidance to not merge PRs autonomously in release command (#11661)

Browse source 
This PR adds explicit guidance to the `/release` command that Claude
should never merge PRs autonomously during the release process - always
wait for the user to do it.

🤖 Prepared with Claude Code
This commit is contained in:
Kim Morrison 2025-12-14 16:17:42 +11:00 • committed by GitHub
parent b7e6862163
commit c20378682e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.claude/commands/release.md
View file

@ -39,6 +39,7 @@ These comments explain the scripts' behavior, which repositories get special han
## Important Notes
- **NEVER merge PRs autonomously** - always wait for the user to merge PRs themselves
- The `release_steps.py` script is idempotent - it's safe to rerun
- The `release_checklist.py` script is idempotent - it's safe to rerun
- Some repositories depend on others (e.g., mathlib4 depends on batteries, aesop, etc.)