open-mpi / ompi

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

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

Closed fullerdj closed 3 months ago

fullerdj commented 3 months ago

Cornelius -> Cornelis

github-actions[bot] commented 3 months ago

Hello! The Git Commit Checker CI bot found a few problems with this PR:

41122c40: docs/../ofi.rst: Correct typographical error

Please fix these problems and, if necessary, force-push new commits back up to the PR branch. Thanks!

jsquyres commented 3 months ago

@fullerdj Can you include the (cherry picked from ...) line in your commit message? It helps us track what we've brought from main and what we haven't.

You can do it via git cherry pick -x ... or add it manually to the commit message.

Thanks!

EDIT: Disregard... you already did it. 😄