Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

docs/../ofi.rst: Correct typographical error #12761

Merged
merged 1 commit into from
Aug 15, 2024
Merged

Conversation

fullerdj
Copy link
Contributor

Cornelius -> Cornelis

Cornelius -> Cornelis

Signed-off-by: Douglas Fuller <[email protected]>
Copy link
Member

@jsquyres jsquyres left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! Can you cherry-pick to the v5.0.x branch when this merges?

@jsquyres jsquyres merged commit caa54f0 into open-mpi:main Aug 15, 2024
14 checks passed
@fullerdj
Copy link
Contributor Author

Sure. How do you like your history? I probably can't cherry-pick the merge over to that branch (it'll conflict a bunch). Do you just want me to cherry-pick my individual commit and push it there?

@fullerdj
Copy link
Contributor Author

n/m, no real conflicts, I just don't have permission to push to open-mpi. Let me know if you want me to do a PR.

@jsquyres
Copy link
Member

@fullerdj Yes, please just make a PR to the v5.0.x branch. Thanks!

(main and v5.0.x aren't that far apart, even though v5.0.x branched off quite a while ago)

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.

2 participants