2 files changed, 1 insertions, 1 deletions

diff --git a/.file-metadata b/.file-metadata
index 392f66d..9e9f414 100644
--- a/.file-metadata
+++ b/.file-metadata
diff --git a/configure b/configure
index df87435..9975cae 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#! /bin/sh
+#! /bin/bash
 #
 # Necessary preparations/configurations for the reproduction pipeline.
 #