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.

1 files changed, 1 insertions, 1 deletions

diff --git a/bin/clone.sh b/bin/clone.sh
index d1195b3..e40aa11 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