lib/Tools/install
changeset 6082 590f9e3bf4d8
parent 5404 fde117f1006b
child 6417 39941b906910
     1.1 --- a/lib/Tools/install	Mon Jan 11 18:45:46 1999 +0100
     1.2 +++ b/lib/Tools/install	Tue Jan 12 12:17:53 1999 +0100
     1.3 @@ -61,8 +61,8 @@
     1.4  
     1.5  mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
     1.6  
     1.7 -BASH=$(type -path bash)
     1.8 -[ -z "$BASH" ] && fail "Cannot find bash!"
     1.9 +#set by configure
    1.10 +AUTO_BASH=/bin/bash
    1.11  
    1.12  echo "using $DISTDIR"
    1.13  
    1.14 @@ -71,7 +71,7 @@
    1.15    BIN="$BINDIR/$NAME"
    1.16    DIST="$DISTDIR/bin/$NAME"
    1.17    echo "installing $BIN"
    1.18 -  echo "#!$BASH" >$BIN || fail "Cannot write file: $BIN"
    1.19 +  echo "#!$AUTO_BASH" >$BIN || fail "Cannot write file: $BIN"
    1.20    echo >>$BIN
    1.21    echo "exec $DIST \"\$@\"" >>$BIN
    1.22    chmod +x $BIN