From ee04d509f7f449643217793e7a54074de668e53b Mon Sep 17 00:00:00 2001 From: BREW <81044362+b-re-w@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:19:25 +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 4c7cbea..5c7e561 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