dev-shell is a bash script, not sh

'type -p' does not work in e.g. dash
2014-05-23 11:41:09 +08:00 · 2014-05-23 11:41:09 +08:00 · b1d39d4765
parent 8ea9fd7aa6
commit b1d39d4765
1 changed files with 1 additions and 1 deletions
--- a/2
+++ b/2
@ -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