/usr/bin/env bash;
authorwenzelm
Thu, 30 Nov 2000 20:10:29 +0100
changeset 10555 2323ec838401
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
--- a/bin/isabelle	Thu Nov 30 20:07:35 2000 +0100
+++ b/bin/isabelle	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/bin/isatool	Thu Nov 30 20:07:35 2000 +0100
+++ b/bin/isatool	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/build	Thu Nov 30 20:07:35 2000 +0100
+++ b/build	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/browser	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/browser	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/doc	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/doc	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/document	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/document	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/expandshort	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/expandshort	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/findlogics	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/findlogics	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/fixclasimp	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/fixclasimp	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/fixdatatype	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/fixdatatype	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/fixdots	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/fixdots	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/fixgoal	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/fixgoal	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/fixseq	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/fixseq	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/fixsome	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/fixsome	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/getenv	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/getenv	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- 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
--- a/lib/Tools/installfonts	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/installfonts	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/latex	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/latex	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/logo	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/logo	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/make	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/make	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/makeall	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/makeall	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/mkdir	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/mkdir	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/nonascii	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/nonascii	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/symbolinput	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/symbolinput	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/unsymbolize	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/unsymbolize	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/Tools/usedir	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/Tools/usedir	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/feeder	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/feeder	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/isa-emacs	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/isa-emacs	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/isa-xterm	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/isa-xterm	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/run-mlworks	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/run-mlworks	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/run-mosml	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/run-mosml	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/run-polyml	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/run-polyml	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/run-smlnj	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/run-smlnj	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/run-smlnj-0.93	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/run-smlnj-0.93	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
--- a/lib/scripts/showtime	Thu Nov 30 20:07:35 2000 +0100
+++ b/lib/scripts/showtime	Thu Nov 30 20:10:29 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen