Skip to content

Conversation

@devreal
Copy link
Contributor

@devreal devreal commented Jul 27, 2020

Cherry-pick of #7113 to the v4.0.x branch.

Fixes #7967

Signed-off-by: Joseph Schuchart [email protected]
(cherry picked from commit 02dd877)

Signed-off-by: Joseph Schuchart <[email protected]>
(cherry picked from commit 02dd877)
@devreal devreal requested review from bosilca and hjelmn July 27, 2020 14:09
@devreal devreal self-assigned this Jul 27, 2020
@hppritcha hppritcha added the NEWS label Jul 27, 2020
@gpaulsen gpaulsen merged commit 96b9d29 into open-mpi:v4.0.x Jul 27, 2020
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.

4 participants