* Update install openmpi-bin to also install mpi-default-dev instead of libopenmpi-dev. This according to https://bugs.launchpad.net/ubuntu/+source/openmpi/+bug/1870780.
* Update install openmpi-bin to also install mpi-default-dev instead of libopenmpi-dev. This according to https://bugs.launchpad.net/ubuntu/+source/openmpi/+bug/1870780.