On Wed, May 31, 2017 at 9:24 PM, Phil Ruffwind <rf@rufflewind.com> wrote:

> Can you add a ticket about this? Collectives WG seems like the right
> place...

Here? https://github.com/mpiwg-coll/coll-issues

Or here? https://github.com/mpi-forum/mpi-issues/issues