about summary refs log tree commit diff
path: root/dev-shell
diff options
context:
space:
mode:
authorSönke Hahn <soenkehahn@gmail.com>2014-05-23T03·41+0800
committerEelco Dolstra <eelco.dolstra@logicblox.com>2014-05-26T15·21+0200
commitb1d39d476544644b2de8addb5ad3289fede2f95a (patch)
treee7d34224d965f3889d148390b27e6a13d751f7bd /dev-shell
parent8ea9fd7aa6b2152f95724e504ac61c57d90b113c (diff)
dev-shell is a bash script, not sh
'type -p' does not work in e.g. dash
Diffstat (limited to 'dev-shell')
-rwxr-xr-xdev-shell2
1 files changed, 1 insertions, 1 deletions
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