--- 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