--- ./lib/Tools/install.orig	Sun Sep  2 15:11:55 2007
+++ ./lib/Tools/install	Sun Sep  2 15:52:30 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
 #
 # $Id: install,v 1.25 2005/07/01 12:41:57 wenzelm Exp $
 # Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
 
 PRG=$(basename "$0")
 
-function usage()
+usage()
 {
   echo
   echo "Usage: $PRG [OPTIONS]"
@@ -24,7 +24,7 @@
   exit 1
 }
 
-function fail()
+fail()
 {
   echo "$1" >&2
   exit 2
@@ -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 "#!/bin/sh" > "$BIN" || fail "Cannot write file: $BIN"
     echo >> "$BIN"
     echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
     chmod +x "$BIN"