search

open-mpi / ompi

Open MPI main development repository
https://www.open-mpi.org
Other
2.13k stars 858 forks source link

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

Closed fullerdj closed 1 month ago

fullerdj commented 1 month ago

Cornelius -> Cornelis

fullerdj commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

@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)