From b1d39d476544644b2de8addb5ad3289fede2f95a Mon Sep 17 00:00:00 2001
From: Sönke Hahn <soenkehahn@gmail.com>
Date: Fri, 23 May 2014 11:41:09 +0800
Subject: 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(-)

(limited to 'dev-shell')

diff --git a/dev-shell b/dev-shell
index a4fdc6814bd2..2fe62a4696a3 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
-- 
cgit 1.4.1