Configure script starts with bin/bash shebang

While trying the pipeline on a remote server (which runs on Debian), the
configure script had an `Syntax error: "(" unexpected' error. This is
caused by the fact that in the Debian world (and its derivate OSs), the
default shell is not Bash but Dash which has much fewer features for fast
loading. It was thus necessary to start the configure script explicity with
the `/bin/bash' shebang.

1 files changed, 1 insertions, 1 deletions

diff --git a/configure b/configure
index 061a810..e1baae0 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#! /bin/sh
+#! /bin/bash
 #
 # Necessary preparations/configurations for the reproduction pipeline.
 #