# HG changeset patch
# User wenzelm
# Date 975611429 -3600
# Node ID 2323ec838401e76797d91d3b583dd3896db5e2c0
# Parent  81edb1d201ab78605eb4e808abeb15390c23b098
/usr/bin/env bash;

diff -r 81edb1d201ab -r 2323ec838401 bin/isabelle
--- 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
diff -r 81edb1d201ab -r 2323ec838401 bin/isatool
--- 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
diff -r 81edb1d201ab -r 2323ec838401 build
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/browser
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/doc
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/document
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/expandshort
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/findlogics
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/fixclasimp
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/fixdatatype
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/fixdots
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/fixgoal
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/fixseq
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/fixsome
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/getenv
--- 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
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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/installfonts
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/latex
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/logo
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/make
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/makeall
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/mkdir
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/nonascii
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/symbolinput
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/unsymbolize
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/Tools/usedir
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/feeder
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/isa-emacs
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/isa-xterm
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/run-mlworks
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/run-mosml
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/run-polyml
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/run-smlnj
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/run-smlnj-0.93
--- 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
diff -r 81edb1d201ab -r 2323ec838401 lib/scripts/showtime
--- 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