# HG changeset patch
# User wenzelm
# Date 1207662432 -7200
# Node ID 50f47cc2af72256300a058f3a8058be6fdc0ea11
# Parent  fc76b7b79ba9e50236ad1cd809e7caa0436c5b70
removed obsolete AUTO_BASH feature;

diff -r fc76b7b79ba9 -r 50f47cc2af72 lib/Tools/install
--- 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"