From 5c54cf2a633e79104b2c165af4984b6eb9d50c2f Mon Sep 17 00:00:00 2001
From: Donald Buczek <buczek@molgen.mpg.de>
Date: Wed, 13 Jun 2018 16:52:51 +0200
Subject: [PATCH] install.sh: Change interpreter to /bin/bash

/bin/sh is the same as /usr/bin/bash on mariux, but not on
flughafenberlinbrandenburgwillybrandt. Because we use bash syntax, be
explicit here are ask for bash.
---
 install.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/install.sh b/install.sh
index 58a73f9..f930bf3 100755
--- a/install.sh
+++ b/install.sh
@@ -1,4 +1,4 @@
-#! /bin/sh
+#! /bin/bash
 
 # Although these should be inherited from the Makefile,
 # we set some defaults ourself, too, in case we are called