From 6aed8b64cab3a2e6eededb8f733d671f5b996ca7 Mon Sep 17 00:00:00 2001
From: Julian Dax <julian.dax@posteo.de>
Date: Thu, 19 Sep 2019 07:39:27 +0200
Subject: [PATCH] Use #!/bin/bash instead of #!/bin/sh (#6062)

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'