From 724c04813fcb1f961bd691ee3994fb77bb1288df Mon Sep 17 00:00:00 2001 From: BREW <81044362+b-re-w@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:19:04 +0900 Subject: [PATCH] Docs: Close the issue after the develop merge Closes #N only fires on merges into main; feature pull requests merge into develop, so the issue has to be closed explicitly. --- AGENTS.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/AGENTS.md b/AGENTS.md index 266f01da0..1426f3666 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -66,7 +66,10 @@ Every new feature goes through an issue and a pull request: 3. Work on a `work/` branch, push every commit, and open a pull request into `develop` whose body contains `Closes #`. 4. Merge into `develop` through that pull request (`gh pr merge`), not by a local merge, so the - issue is linked and closed. + issue is linked. +5. Then close the issue yourself: `gh issue close --comment "Landed in develop via #"`. + GitHub's `Closes #N` only fires when a pull request merges into the default branch (`main`), + and these pull requests merge into `develop`. ## 5. Intent → Spec → Test → Code