mpi-forum / mpi-issues

Tickets for the MPI Forum
http://www.mpi-forum.org/
67 stars 8 forks source link

change-log entry missing for PR 658 #778

Closed th-hlrs closed 1 month ago

th-hlrs commented 1 year ago

Problem

https://github.com/mpi-forum/mpi-standard/pull/658 should have a change-log entry, currently missing.

wesbland commented 1 month ago

This passed a no-no vote on 2023-12-04.

Yes No Abstain
27 0 3
wesbland commented 1 month ago

This passed an errata vote on 2023-12-05.

Yes No Abstain
24 0 6
wesbland commented 1 month ago

@hppritcha I'm trying to find the PR that went with this issue to make sure it got merged. Can you please help?

hppritcha commented 1 month ago

Looks like there was a PR but it was never merged - https://github.com/mpi-forum/mpi-standard/pull/899

wesbland commented 1 month ago

That might have been a mistake on my part. I guess it was supposed to be merged and not closed?