[Pkg-openmpi-maintainers] Bug#889715: libopenmpi-dev: problem in alternatives handling

[Andreas Beckmann]

Followup-For: Bug #889715

Hi,

I wanted to look into this, but debian/libopenmpi-dev.postinst.in in git
contains an unresolved but committed mismerge (with <<<<<<< ======= >>>>>>>
markers). Stopping here.


Andreas