Skip to content

chore: sync main to dev - #9683

Merged
dalkia merged 1 commit into
devfrom
chore/sync
Aug 12, 2026
Merged

chore: sync main to dev#9683
dalkia merged 1 commit into
devfrom
chore/sync

Conversation

@github-actions

Copy link
Copy Markdown
Contributor

👑 An automated PR

Important

This PR must be merged by an admin, as a merge commit ("Merge pull request", bypassing the linear-history rule) — never squash or rebase it.
Squashing rewrites the synced commits, which makes main and dev diverge silently and surfaces later as release-merge conflicts.
The enforce-approvals required check stays red until an admin approves this PR.

This manual procedure has kept main and dev in sync for years when followed — see #9566 for the mechanical enforcement plan (ruleset + bot bypass) we will apply if a squash slips through again.

@dalkia
dalkia merged commit bb56416 into dev Aug 12, 2026
57 of 60 checks passed
@dalkia
dalkia deleted the chore/sync branch August 12, 2026 10:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants