Skip to content

Conversation

@jsquyres
Copy link
Member

(cherry picked from commit a6b8cd3)

This is a v5.0.x PR corresponding to main PR #13438. Thanks to @charlesgwaldman for the submission.

Signed-off-by: charlesgwaldman <120225331+charlesgwaldman@users.noreply.github.com>
(cherry picked from commit a6b8cd3)
@github-actions github-actions bot added this to the v5.0.8 milestone Oct 15, 2025
@janjust janjust merged commit 04d592f into open-mpi:v5.0.x Oct 15, 2025
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants