From eed3f2f2820b4d28bf77c05fc945f3c56ac2a2ef Mon Sep 17 00:00:00 2001
From: Julian Dax <julian.dax@posteo.de>
Date: Wed, 18 Sep 2019 15:11:27 +0200
Subject: [PATCH] Use #!/bin/bash instead of #!/bin/sh

The script uses double square brackets, which are a non-standard extension to `[]`. Some shells (e.g. dash, the default shell under Debian) do not support double square brackets. The shebang line should reflect that.
---
 bootstrap.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bootstrap.sh b/bootstrap.sh
index 3f8b3db6ed..9446016d80 100755
--- a/bootstrap.sh
+++ b/bootstrap.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 RED='\033[0;31m'
 GREEN='\033[0;32m'
 NC='\033[0m'