5a35a8e82c
Fixes open-mpi/ompi#3522 Signed-off-by: Gilles Gouaillardet <gilles@rist.or.jp>
Fixes open-mpi/ompi#3522 Signed-off-by: Gilles Gouaillardet <gilles@rist.or.jp>