From b9fc1c35dd8344aa78e29c6cc68acc6203ef66f8 Mon Sep 17 00:00:00 2001
From: Mohammad Akhlaghi <mohammad@akhlaghi.org>
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.
---
 .file-metadata | Bin 3714 -> 3714 bytes
 configure      |   2 +-
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/.file-metadata b/.file-metadata
index 392f66d..9e9f414 100644
Binary files a/.file-metadata and b/.file-metadata differ
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