/usr/bin/env bash;
authorwenzelm
Thu Nov 30 20:10:29 2000 +0100 (2000-11-30)
changeset 105552323ec838401
parent 10554 81edb1d201ab
child 10556 e574274823a4
/usr/bin/env bash;
bin/isabelle
bin/isatool
build
lib/Tools/browser
lib/Tools/doc
lib/Tools/document
lib/Tools/expandshort
lib/Tools/findlogics
lib/Tools/fixclasimp
lib/Tools/fixdatatype
lib/Tools/fixdots
lib/Tools/fixgoal
lib/Tools/fixseq
lib/Tools/fixsome
lib/Tools/getenv
lib/Tools/install
lib/Tools/installfonts
lib/Tools/latex
lib/Tools/logo
lib/Tools/make
lib/Tools/makeall
lib/Tools/mkdir
lib/Tools/nonascii
lib/Tools/symbolinput
lib/Tools/unsymbolize
lib/Tools/usedir
lib/scripts/feeder
lib/scripts/isa-emacs
lib/scripts/isa-xterm
lib/scripts/run-mlworks
lib/scripts/run-mosml
lib/scripts/run-polyml
lib/scripts/run-smlnj
lib/scripts/run-smlnj-0.93
lib/scripts/showtime
     1.1 --- a/bin/isabelle	Thu Nov 30 20:07:35 2000 +0100
     1.2 +++ b/bin/isabelle	Thu Nov 30 20:10:29 2000 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -#!/bin/bash
     1.5 +#!/usr/bin/env bash
     1.6  #
     1.7  # $Id$
     1.8  # Author: Markus Wenzel, TU Muenchen
     2.1 --- a/bin/isatool	Thu Nov 30 20:07:35 2000 +0100
     2.2 +++ b/bin/isatool	Thu Nov 30 20:10:29 2000 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -#!/bin/bash
     2.5 +#!/usr/bin/env bash
     2.6  #
     2.7  # $Id$
     2.8  # Author: Markus Wenzel, TU Muenchen
     3.1 --- a/build	Thu Nov 30 20:07:35 2000 +0100
     3.2 +++ b/build	Thu Nov 30 20:10:29 2000 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -#!/bin/bash
     3.5 +#!/usr/bin/env bash
     3.6  #
     3.7  # $Id$
     3.8  # Author: Markus Wenzel, TU Muenchen
     4.1 --- a/lib/Tools/browser	Thu Nov 30 20:07:35 2000 +0100
     4.2 +++ b/lib/Tools/browser	Thu Nov 30 20:10:29 2000 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -#!/bin/bash
     4.5 +#!/usr/bin/env bash
     4.6  #
     4.7  # $Id$
     4.8  # Author: Markus Wenzel, TU Muenchen
     5.1 --- a/lib/Tools/doc	Thu Nov 30 20:07:35 2000 +0100
     5.2 +++ b/lib/Tools/doc	Thu Nov 30 20:10:29 2000 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -#!/bin/bash
     5.5 +#!/usr/bin/env bash
     5.6  #
     5.7  # $Id$
     5.8  # Author: Markus Wenzel, TU Muenchen
     6.1 --- a/lib/Tools/document	Thu Nov 30 20:07:35 2000 +0100
     6.2 +++ b/lib/Tools/document	Thu Nov 30 20:10:29 2000 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -#!/bin/bash
     6.5 +#!/usr/bin/env bash
     6.6  #
     6.7  # $Id$
     6.8  # Author: Markus Wenzel, TU Muenchen
     7.1 --- a/lib/Tools/expandshort	Thu Nov 30 20:07:35 2000 +0100
     7.2 +++ b/lib/Tools/expandshort	Thu Nov 30 20:10:29 2000 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -#!/bin/bash
     7.5 +#!/usr/bin/env bash
     7.6  #
     7.7  # $Id$
     7.8  # Author: Markus Wenzel, TU Muenchen
     8.1 --- a/lib/Tools/findlogics	Thu Nov 30 20:07:35 2000 +0100
     8.2 +++ b/lib/Tools/findlogics	Thu Nov 30 20:10:29 2000 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -#!/bin/bash
     8.5 +#!/usr/bin/env bash
     8.6  #
     8.7  # $Id$
     8.8  # Author: Markus Wenzel, TU Muenchen
     9.1 --- a/lib/Tools/fixclasimp	Thu Nov 30 20:07:35 2000 +0100
     9.2 +++ b/lib/Tools/fixclasimp	Thu Nov 30 20:10:29 2000 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -#!/bin/bash
     9.5 +#!/usr/bin/env bash
     9.6  #
     9.7  # $Id$
     9.8  # Author: Markus Wenzel, TU Muenchen
    10.1 --- a/lib/Tools/fixdatatype	Thu Nov 30 20:07:35 2000 +0100
    10.2 +++ b/lib/Tools/fixdatatype	Thu Nov 30 20:10:29 2000 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -#!/bin/bash
    10.5 +#!/usr/bin/env bash
    10.6  #
    10.7  # $Id$
    10.8  # Author: Markus Wenzel, TU Muenchen
    11.1 --- a/lib/Tools/fixdots	Thu Nov 30 20:07:35 2000 +0100
    11.2 +++ b/lib/Tools/fixdots	Thu Nov 30 20:10:29 2000 +0100
    11.3 @@ -1,4 +1,4 @@
    11.4 -#!/bin/bash
    11.5 +#!/usr/bin/env bash
    11.6  #
    11.7  # $Id$
    11.8  # Author: Markus Wenzel, TU Muenchen
    12.1 --- a/lib/Tools/fixgoal	Thu Nov 30 20:07:35 2000 +0100
    12.2 +++ b/lib/Tools/fixgoal	Thu Nov 30 20:10:29 2000 +0100
    12.3 @@ -1,4 +1,4 @@
    12.4 -#!/bin/bash
    12.5 +#!/usr/bin/env bash
    12.6  #
    12.7  # $Id$
    12.8  # Author: Markus Wenzel, TU Muenchen
    13.1 --- a/lib/Tools/fixseq	Thu Nov 30 20:07:35 2000 +0100
    13.2 +++ b/lib/Tools/fixseq	Thu Nov 30 20:10:29 2000 +0100
    13.3 @@ -1,4 +1,4 @@
    13.4 -#!/bin/bash
    13.5 +#!/usr/bin/env bash
    13.6  #
    13.7  # $Id$
    13.8  # Author: Markus Wenzel, TU Muenchen
    14.1 --- a/lib/Tools/fixsome	Thu Nov 30 20:07:35 2000 +0100
    14.2 +++ b/lib/Tools/fixsome	Thu Nov 30 20:10:29 2000 +0100
    14.3 @@ -1,4 +1,4 @@
    14.4 -#!/bin/bash
    14.5 +#!/usr/bin/env bash
    14.6  #
    14.7  # $Id$
    14.8  # Author: Markus Wenzel, TU Muenchen
    15.1 --- a/lib/Tools/getenv	Thu Nov 30 20:07:35 2000 +0100
    15.2 +++ b/lib/Tools/getenv	Thu Nov 30 20:10:29 2000 +0100
    15.3 @@ -1,4 +1,4 @@
    15.4 -#!/bin/bash
    15.5 +#!/usr/bin/env bash
    15.6  #
    15.7  # $Id$
    15.8  # Author: Markus Wenzel, TU Muenchen
    16.1 --- a/lib/Tools/install	Thu Nov 30 20:07:35 2000 +0100
    16.2 +++ b/lib/Tools/install	Thu Nov 30 20:10:29 2000 +0100
    16.3 @@ -1,4 +1,4 @@
    16.4 -#!/bin/bash
    16.5 +#!/usr/bin/env bash
    16.6  #
    16.7  # $Id$
    16.8  # Author: Markus Wenzel, TU Muenchen
    16.9 @@ -80,7 +80,16 @@
   16.10  # standalone binaries
   16.11  
   16.12  #set by configure
   16.13 -AUTO_BASH=/bin/bash
   16.14 +AUTO_BASH=bash
   16.15 +
   16.16 +case "$AUTO_BASH" in
   16.17 +  /*)
   16.18 +    BASH="$AUTO_BASH"
   16.19 +    ;;
   16.20 +  *)
   16.21 +    BASH="/usr/bin/env bash"
   16.22 +    ;;
   16.23 +esac
   16.24  
   16.25  if [ -n "$BINDIR" ]; then
   16.26    mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
   16.27 @@ -90,7 +99,7 @@
   16.28      BIN="$BINDIR/$NAME"
   16.29      DIST="$DISTDIR/bin/$NAME"
   16.30      echo "installing $BIN"
   16.31 -    echo "#!$AUTO_BASH" > "$BIN" || fail "Cannot write file: $BIN"
   16.32 +    echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
   16.33      echo >> "$BIN"
   16.34      echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
   16.35      chmod +x "$BIN"
   16.36 @@ -125,5 +134,6 @@
   16.37    echo "Terminal=0" >> "$KDEAPP"
   16.38    echo "Name=Isabelle" >> "$KDEAPP"
   16.39  
   16.40 +  echo
   16.41    echo "Please refresh your KDE desktop now!"
   16.42  fi
    17.1 --- a/lib/Tools/installfonts	Thu Nov 30 20:07:35 2000 +0100
    17.2 +++ b/lib/Tools/installfonts	Thu Nov 30 20:10:29 2000 +0100
    17.3 @@ -1,4 +1,4 @@
    17.4 -#!/bin/bash
    17.5 +#!/usr/bin/env bash
    17.6  #
    17.7  # $Id$
    17.8  # Author: Markus Wenzel, TU Muenchen
    18.1 --- a/lib/Tools/latex	Thu Nov 30 20:07:35 2000 +0100
    18.2 +++ b/lib/Tools/latex	Thu Nov 30 20:10:29 2000 +0100
    18.3 @@ -1,4 +1,4 @@
    18.4 -#!/bin/bash
    18.5 +#!/usr/bin/env bash
    18.6  #
    18.7  # $Id$
    18.8  # Author: Markus Wenzel, TU Muenchen
    19.1 --- a/lib/Tools/logo	Thu Nov 30 20:07:35 2000 +0100
    19.2 +++ b/lib/Tools/logo	Thu Nov 30 20:10:29 2000 +0100
    19.3 @@ -1,4 +1,4 @@
    19.4 -#!/bin/bash
    19.5 +#!/usr/bin/env bash
    19.6  #
    19.7  # $Id$
    19.8  # Author: Markus Wenzel, TU Muenchen
    20.1 --- a/lib/Tools/make	Thu Nov 30 20:07:35 2000 +0100
    20.2 +++ b/lib/Tools/make	Thu Nov 30 20:10:29 2000 +0100
    20.3 @@ -1,4 +1,4 @@
    20.4 -#!/bin/bash
    20.5 +#!/usr/bin/env bash
    20.6  #
    20.7  # $Id$
    20.8  # Author: Markus Wenzel, TU Muenchen
    21.1 --- a/lib/Tools/makeall	Thu Nov 30 20:07:35 2000 +0100
    21.2 +++ b/lib/Tools/makeall	Thu Nov 30 20:10:29 2000 +0100
    21.3 @@ -1,4 +1,4 @@
    21.4 -#!/bin/bash
    21.5 +#!/usr/bin/env bash
    21.6  #
    21.7  # $Id$
    21.8  # Author: Markus Wenzel, TU Muenchen
    22.1 --- a/lib/Tools/mkdir	Thu Nov 30 20:07:35 2000 +0100
    22.2 +++ b/lib/Tools/mkdir	Thu Nov 30 20:10:29 2000 +0100
    22.3 @@ -1,4 +1,4 @@
    22.4 -#!/bin/bash
    22.5 +#!/usr/bin/env bash
    22.6  #
    22.7  # $Id$
    22.8  # Author: Markus Wenzel, TU Muenchen
    23.1 --- a/lib/Tools/nonascii	Thu Nov 30 20:07:35 2000 +0100
    23.2 +++ b/lib/Tools/nonascii	Thu Nov 30 20:10:29 2000 +0100
    23.3 @@ -1,4 +1,4 @@
    23.4 -#!/bin/bash
    23.5 +#!/usr/bin/env bash
    23.6  #
    23.7  # $Id$
    23.8  # Author: Markus Wenzel, TU Muenchen
    24.1 --- a/lib/Tools/symbolinput	Thu Nov 30 20:07:35 2000 +0100
    24.2 +++ b/lib/Tools/symbolinput	Thu Nov 30 20:10:29 2000 +0100
    24.3 @@ -1,4 +1,4 @@
    24.4 -#!/bin/bash
    24.5 +#!/usr/bin/env bash
    24.6  #
    24.7  # $Id$
    24.8  # Author: Markus Wenzel, TU Muenchen
    25.1 --- a/lib/Tools/unsymbolize	Thu Nov 30 20:07:35 2000 +0100
    25.2 +++ b/lib/Tools/unsymbolize	Thu Nov 30 20:10:29 2000 +0100
    25.3 @@ -1,4 +1,4 @@
    25.4 -#!/bin/bash
    25.5 +#!/usr/bin/env bash
    25.6  #
    25.7  # $Id$
    25.8  # Author: Markus Wenzel, TU Muenchen
    26.1 --- a/lib/Tools/usedir	Thu Nov 30 20:07:35 2000 +0100
    26.2 +++ b/lib/Tools/usedir	Thu Nov 30 20:10:29 2000 +0100
    26.3 @@ -1,4 +1,4 @@
    26.4 -#!/bin/bash
    26.5 +#!/usr/bin/env bash
    26.6  #
    26.7  # $Id$
    26.8  # Author: Markus Wenzel, TU Muenchen
    27.1 --- a/lib/scripts/feeder	Thu Nov 30 20:07:35 2000 +0100
    27.2 +++ b/lib/scripts/feeder	Thu Nov 30 20:10:29 2000 +0100
    27.3 @@ -1,4 +1,4 @@
    27.4 -#!/bin/bash
    27.5 +#!/usr/bin/env bash
    27.6  #
    27.7  # $Id$
    27.8  # Author: Markus Wenzel, TU Muenchen
    28.1 --- a/lib/scripts/isa-emacs	Thu Nov 30 20:07:35 2000 +0100
    28.2 +++ b/lib/scripts/isa-emacs	Thu Nov 30 20:10:29 2000 +0100
    28.3 @@ -1,4 +1,4 @@
    28.4 -#!/bin/bash
    28.5 +#!/usr/bin/env bash
    28.6  #
    28.7  # $Id$
    28.8  # Author: Markus Wenzel, TU Muenchen
    29.1 --- a/lib/scripts/isa-xterm	Thu Nov 30 20:07:35 2000 +0100
    29.2 +++ b/lib/scripts/isa-xterm	Thu Nov 30 20:10:29 2000 +0100
    29.3 @@ -1,4 +1,4 @@
    29.4 -#!/bin/bash
    29.5 +#!/usr/bin/env bash
    29.6  #
    29.7  # $Id$
    29.8  # Author: Markus Wenzel, TU Muenchen
    30.1 --- a/lib/scripts/run-mlworks	Thu Nov 30 20:07:35 2000 +0100
    30.2 +++ b/lib/scripts/run-mlworks	Thu Nov 30 20:10:29 2000 +0100
    30.3 @@ -1,4 +1,4 @@
    30.4 -#!/bin/bash
    30.5 +#!/usr/bin/env bash
    30.6  #
    30.7  # $Id$
    30.8  # Author: Markus Wenzel, TU Muenchen
    31.1 --- a/lib/scripts/run-mosml	Thu Nov 30 20:07:35 2000 +0100
    31.2 +++ b/lib/scripts/run-mosml	Thu Nov 30 20:10:29 2000 +0100
    31.3 @@ -1,4 +1,4 @@
    31.4 -#!/bin/bash
    31.5 +#!/usr/bin/env bash
    31.6  #
    31.7  # $Id$
    31.8  # Author: Markus Wenzel, TU Muenchen
    32.1 --- a/lib/scripts/run-polyml	Thu Nov 30 20:07:35 2000 +0100
    32.2 +++ b/lib/scripts/run-polyml	Thu Nov 30 20:10:29 2000 +0100
    32.3 @@ -1,4 +1,4 @@
    32.4 -#!/bin/bash
    32.5 +#!/usr/bin/env bash
    32.6  #
    32.7  # $Id$
    32.8  # Author: Markus Wenzel, TU Muenchen
    33.1 --- a/lib/scripts/run-smlnj	Thu Nov 30 20:07:35 2000 +0100
    33.2 +++ b/lib/scripts/run-smlnj	Thu Nov 30 20:10:29 2000 +0100
    33.3 @@ -1,4 +1,4 @@
    33.4 -#!/bin/bash
    33.5 +#!/usr/bin/env bash
    33.6  #
    33.7  # $Id$
    33.8  # Author: Markus Wenzel, TU Muenchen
    34.1 --- a/lib/scripts/run-smlnj-0.93	Thu Nov 30 20:07:35 2000 +0100
    34.2 +++ b/lib/scripts/run-smlnj-0.93	Thu Nov 30 20:10:29 2000 +0100
    34.3 @@ -1,4 +1,4 @@
    34.4 -#!/bin/bash
    34.5 +#!/usr/bin/env bash
    34.6  #
    34.7  # $Id$
    34.8  # Author: Markus Wenzel, TU Muenchen
    35.1 --- a/lib/scripts/showtime	Thu Nov 30 20:07:35 2000 +0100
    35.2 +++ b/lib/scripts/showtime	Thu Nov 30 20:10:29 2000 +0100
    35.3 @@ -1,4 +1,4 @@
    35.4 -#!/bin/bash
    35.5 +#!/usr/bin/env bash
    35.6  #
    35.7  # $Id$
    35.8  # Author: Markus Wenzel, TU Muenchen