Shell to run configure script set to /bin/sh

We had previously started the `configure' script with `/bin/bash'. But this
script is meant to check for Bash inside of it. So to be run-able (on a
system which may not have Bash), the `configure' script has to be run by
`/bin/sh'.

1 files changed, 1 insertions, 1 deletions

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