From 12777c75de013df0cab2e4dd93518e817cea0b1e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ivan=20Vu=C4=8Dica?= <ivan@vucica.net>
Date: Thu, 19 Nov 2015 14:03:33 +0000
Subject: [PATCH] clone.sh should use bash due to bashisms

Bashisms pushd/popd don't work so well if /bin/sh is dash, as is the case on a Debian machine.
---
 bin/clone.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/clone.sh b/bin/clone.sh
index d1195b3f..e40aa117 100755
--- a/bin/clone.sh
+++ b/bin/clone.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 if [ "$#" -ne 1 ] || ! [ -d "$1" ]; then
   echo "Usage: $0 DIRECTORY_TO_CLONE_INTO" >&2