From b9fc1c35dd8344aa78e29c6cc68acc6203ef66f8 Mon Sep 17 00:00:00 2001 From: Mohammad Akhlaghi Date: Fri, 1 Feb 2019 10:02:04 +0000 Subject: Configure script now runs under /bin/bash Until now it was `/bin/sh', but on Debian systems, this can cause problems because by default they use a much weaker shell (dash) which doesn't recognize functions. --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'configure') 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. # -- cgit v1.2.1