From b1d39d476544644b2de8addb5ad3289fede2f95a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=B6nke=20Hahn?= <soenkehahn@gmail.com>
Date: Fri, 23 May 2014 11:41:09 +0800
Subject: [PATCH] dev-shell is a bash script, not sh

'type -p' does not work in e.g. dash
---
 dev-shell | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev-shell b/dev-shell
index a4fdc6814..2fe62a469 100755
--- a/dev-shell
+++ b/dev-shell
@@ -1,4 +1,4 @@
-#! /bin/sh
+#!/usr/bin/env bash
 if [ -e tests/test-tmp ]; then
     chmod -R u+w tests/test-tmp
     rm -rf tests/test-tmp