From 3b74e0f2756d4220eabbd57d3cc7c2cb12055699 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20L=C3=A4ndle?= <alaendle@users.noreply.github.com>
Date: Mon, 29 Jan 2024 20:24:30 +0100
Subject: [PATCH] Install `libopenmpi-dev` for `mpi-hs`.

---
 docker/02-apt-get-install.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/docker/02-apt-get-install.sh b/docker/02-apt-get-install.sh
index d3e78080..18db3227 100755
--- a/docker/02-apt-get-install.sh
+++ b/docker/02-apt-get-install.sh
@@ -91,6 +91,7 @@ apt-get install -y \
     libnotify-dev \
     liboath-dev \
     libopenal-dev \
+    libopenmpi-dev \
     libpango1.0-dev \
     libpcap0.8-dev \
     libpcre2-dev \