diff options
author | Sönke Hahn <soenkehahn@gmail.com> | 2014-05-23 11:41:09 +0800 |
---|---|---|
committer | Eelco Dolstra <eelco.dolstra@logicblox.com> | 2014-05-26 17:21:20 +0200 |
commit | b1d39d476544644b2de8addb5ad3289fede2f95a (patch) | |
tree | e7d34224d965f3889d148390b27e6a13d751f7bd | |
parent | 8ea9fd7aa6b2152f95724e504ac61c57d90b113c (diff) | |
download | guix-b1d39d476544644b2de8addb5ad3289fede2f95a.tar.gz |
dev-shell is a bash script, not sh
'type -p' does not work in e.g. dash
-rwxr-xr-x | dev-shell | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev-shell b/dev-shell index a4fdc6814b..2fe62a4696 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 |