diff options
-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 |