Skip to content

merge(repo): integrate through pull requests - #1

Merged
LittleCoinCoin merged 2 commits into
mainfrom
ci/pull-requests
Oct 29, 2026
Merged

LittleCoinCoin merged 2 commits into
mainfrom
ci/pull-requests

Conversation

@LittleCoinCoin

Copy link
Copy Markdown
Member

main now changes only through pull requests, as Eliott decided on 2026-10-29. A merge is a push to main, which runs the gates, the commit check and the release.

  • CI runs on pull requests and on pushes to main. Branch pushes are covered by the pull request run.
  • CI checks a pull request's title as the merge commit's subject (merge(<scope>): …), and again whenever the title is edited.
  • CONTRIBUTING describes the flow: open a pull request, rebase before merging, merge with a merge commit, then pull main.

The repository settings already match: only merge commits are allowed, the merge commit's title and body come from the pull request, and merged branches are deleted.

Co-Authored-By: Claude Opus 5.5 noreply@anthropic.com

🤖 Generated with Claude Code

LittleCoinCoin and others added 2 commits October 29, 2026 15:31
A pull request title becomes the merge commit subject, so CI checks it
as one, and again when the title is edited. Branch pushes no longer run
CI on their own: the pull request run covers them.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@LittleCoinCoin
LittleCoinCoin merged commit 585e8de into main Oct 29, 2026
3 checks passed
@LittleCoinCoin
LittleCoinCoin deleted the ci/pull-requests branch October 29, 2026 07:02
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