diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/install
--- a/lib/Tools/install	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/install	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
@@ -80,7 +80,16 @@
 # standalone binaries
 
 #set by configure
-AUTO_BASH=/bin/bash
+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"
@@ -90,7 +99,7 @@
     BIN="$BINDIR/$NAME"
     DIST="$DISTDIR/bin/$NAME"
     echo "installing $BIN"
-    echo "#!$AUTO_BASH" > "$BIN" || fail "Cannot write file: $BIN"
+    echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
     echo >> "$BIN"
     echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
     chmod +x "$BIN"
@@ -125,5 +134,6 @@
   echo "Terminal=0" >> "$KDEAPP"
   echo "Name=Isabelle" >> "$KDEAPP"
 
+  echo
   echo "Please refresh your KDE desktop now!"
 fi