Skip to content

ci: point the push gate at develop after dev → develop rename#36

Merged
mibrahimdev merged 1 commit into
developfrom
ci/correct-develop-push-trigger
Jun 17, 2026
Merged

ci: point the push gate at develop after dev → develop rename#36
mibrahimdev merged 1 commit into
developfrom
ci/correct-develop-push-trigger

Conversation

@mibrahimdev

Copy link
Copy Markdown
Owner

The development trunk was renamed devdevelop (now the GitHub default branch). My earlier flow-setup commit wired build.yml's push trigger to a now-dead dev ref.

This corrects the push trigger to [main, develop] so direct pushes to the integration trunk are gated by build+test. PRs were already gated regardless of base branch. Pages deploy (pages.yml) and the tag-driven Maven Central publish stay pinned to main — releases are cut from main.

🤖 Generated with Claude Code

The development trunk was renamed dev → develop (now the GitHub default
branch). The earlier commit wired the build+test push trigger to a now-dead
`dev` ref; correct it to `develop` so direct pushes to the trunk are gated.
Pages deploy and the tag-driven publish stay on main.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@mibrahimdev mibrahimdev merged commit c03182a into develop Jun 17, 2026
2 of 4 checks passed
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