Skip to content

Merge main into dev after divergence#340

Merged
jhnaldo merged 0 commit into
devfrom
main
Jul 6, 2026
Merged

Merge main into dev after divergence#340
jhnaldo merged 0 commit into
devfrom
main

Conversation

@stonechoe

Copy link
Copy Markdown
Member

Description

#339 was merged directly into main without going through dev, while #331 were added to dev in parallel. As a result, the two branches have diverged.

This PR merges main back into dev.

@jhnaldo jhnaldo merged commit 7d237fd into dev Jul 6, 2026
12 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.

2 participants