lib/Tools/install
changeset 26577 50f47cc2af72
parent 16653 c12c2f411f77
child 28504 7ad7d7d6df47
--- a/lib/Tools/install	Tue Apr 08 15:47:10 2008 +0200
+++ b/lib/Tools/install	Tue Apr 08 15:47:12 2008 +0200
@@ -71,18 +71,6 @@
 
 # standalone binaries
 
-#set by configure
-AUTO_BASH=bash
-
-case "$AUTO_BASH" in
-  /*)
-    BASH="$AUTO_BASH"
-    ;;
-  *)
-    BASH="/usr/bin/env bash"
-    ;;
-esac
-
 if [ -n "$BINDIR" ]; then
   mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
 
@@ -92,7 +80,7 @@
     DIST="$DISTDIR/bin/$NAME"
     echo "installing $BIN"
     rm -f "$BIN"
-    echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
+    echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"
     echo >> "$BIN"
     echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
     chmod +x "$BIN"