open-mpi / ompi

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

OSHMEM installs man pages even if --disable-oshmem is used #850

Closed jsquyres closed 9 years ago

jsquyres commented 9 years ago

@miked-mellanox @jladd-mlnx Can someone at Mellanox have a look?

Thanks.

mike-dubman commented 9 years ago

@igor-ivanov - could you please take a look. thanks

hppritcha commented 9 years ago

@igor-ivanov can this issue be closed?

igor-ivanov commented 9 years ago

@hppritcha yes