dist/tools: Use bash instead of sh where needed

A number of scripts use features from bash such as `local` which are not
in the POSIX spec. This breaks on systems where sh is not symlinked to
bash.

This patch changes the interpreter indicated by the hashbang to bash for
those scripts

dist/tools/ci/print_toolchain_versions.sh

@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 MAKE=${MAKE:-make}
 

dist/tools/coccinelle/check.sh

@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 # Copyright 2017 Kaspar Schleiser <kaspar@schleiser.de>
 #

dist/tools/dlcache/dlcache.sh

@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 DLCACHE_DIR=${DLCACHE_DIR:-~/.dlcache}
 

dist/tools/git/git-cache

@@ -1,4 +1,4 @@
-#!/bin/sh -e
+#!/bin/bash -e
 
 [ "$GIT_CACHE_VERBOSE" != "1" ] && Q=-q
 

dist/tools/licenses/check.sh

@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 # Copyright 2017 Kaspar Schleiser <kaspar@schleiser.de>
 # Copyright 2014 Ludwig Knüpfer <ludwig.knuepfer@fu-berlin.de>