Skip to content

docs(fork): say that GitHub marks the sync pull request merged when main moves - #40

Merged
martinothamar merged 1 commit into
mainfrom
docs/sync-pr-merged
Oct 24, 2026
Merged

martinothamar merged 1 commit into
mainfrom
docs/sync-pr-merged

Conversation

@martinothamar

Copy link
Copy Markdown
Owner

Step 7 of the rewrite in agents/dev/instructions.md said to close the review pull request after force-pushing sync/<date> to main. That can't be done. The push makes the pull request's head main's tip, so GitHub marks it merged, and gh pr close refuses: "can't be closed because it was already merged". Agents keep running into this and stop to work out why, as happened when applying #39.

Step 7 now says that GitHub marks the pull request merged, so it needs no closing, and to comment that the rewrite is applied.

Only agents/dev/instructions.md changes. Prettier passes on it. Per the fork's process, this lands on main as a squash merge and folds into the setup commit at the next rewrite.

…ain moves

Force-pushing a sync branch to main makes the review pull request's head
main's tip, so GitHub marks it merged and gh pr close refuses it. Step 7
said to close it, which sent agents to check why it could not be closed.
@martinothamar
martinothamar merged commit d4dbb5e into main Oct 24, 2026
17 checks passed
@martinothamar
martinothamar deleted the docs/sync-pr-merged branch October 24, 2026 21:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant