12/376: dev-shell is a bash script, not sh

[Ludovic Courtès]

civodul pushed a commit to tag 1.8
in repository guix.

commit b1d39d476544644b2de8addb5ad3289fede2f95a
Author: Sönke Hahn <address@hidden>
Date:   Fri May 23 11:41:09 2014 +0800

    dev-shell is a bash script, not sh
    
    'type -p' does not work in e.g. dash
---
 dev-shell |    2 +-
 1 files changed, 1 insertions(+), 1 deletions(-)

diff --git a/dev-shell b/dev-shell
index a4fdc68..2fe62a4 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