From 2d0357b3939dda9fa958c2c0ba97e366129df602 Mon Sep 17 00:00:00 2001 From: Mohammad Akhlaghi Date: Sat, 11 Aug 2018 14:55:38 +0200 Subject: 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'. --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. # -- cgit v1.2.1