diff options
| author | Sönke Hahn <soenkehahn@gmail.com> | 2014-05-23T03·41+0800 |
|---|---|---|
| committer | Eelco Dolstra <eelco.dolstra@logicblox.com> | 2014-05-26T15·21+0200 |
| commit | b1d39d476544644b2de8addb5ad3289fede2f95a (patch) | |
| tree | e7d34224d965f3889d148390b27e6a13d751f7bd /dev-shell | |
| parent | 8ea9fd7aa6b2152f95724e504ac61c57d90b113c (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-x | dev-shell | 2 |
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 |