Skip to content

Merge master to develop.#534

Merged
ricejasonf merged 1 commit into
developfrom
master
May 24, 2025
Merged

Merge master to develop.#534
ricejasonf merged 1 commit into
developfrom
master

Conversation

@grafikrobot

@grafikrobot grafikrobot commented May 24, 2025

Copy link
Copy Markdown
Member

This solely contains the commits to merge master to develop. Keeping develop up to date is a requirement of the Boost development procedures. Please merge this PR immediately.

Fixes #533

@grafikrobot

Copy link
Copy Markdown
Member Author

FYI, @ldionne

@ricejasonf ricejasonf merged commit 275ee33 into develop May 24, 2025
3 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