# HG changeset patch
# User wenzelm
# Date 916139873 -3600
# Node ID 590f9e3bf4d8dc977f3d59b2fabbf8e6aec7ce09
# Parent  aa97eb904692952bb5cf90331506e35392a2f363
configure AUTO_BASH, AUTO_PERL;

diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/expandshort
--- a/lib/Tools/expandshort	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/expandshort	Tue Jan 12 12:17:53 1999 +0100
@@ -32,4 +32,7 @@
 
 ## main
 
-find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/expandshort.pl
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/expandshort.pl
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/fixclasimp
--- a/lib/Tools/fixclasimp	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/fixclasimp	Tue Jan 12 12:17:53 1999 +0100
@@ -32,4 +32,7 @@
 
 ## main
 
-find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/fixdatatype
--- a/lib/Tools/fixdatatype	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/fixdatatype	Tue Jan 12 12:17:53 1999 +0100
@@ -32,5 +32,8 @@
 
 ## main
 
+#set by configure
+AUTO_PERL=perl
+
 find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
-  xargs perl -w $ISABELLE_HOME/lib/scripts/fixdatatype.pl
+  xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdatatype.pl
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/fixdots
--- a/lib/Tools/fixdots	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/fixdots	Tue Jan 12 12:17:53 1999 +0100
@@ -32,5 +32,8 @@
 
 ## main
 
+#set by configure
+AUTO_PERL=perl
+
 find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
-  xargs perl -w $ISABELLE_HOME/lib/scripts/fixdots.pl
+  xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdots.pl
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/fixgoal
--- a/lib/Tools/fixgoal	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/fixgoal	Tue Jan 12 12:17:53 1999 +0100
@@ -32,4 +32,7 @@
 
 ## main
 
-find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixgoal.pl
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixgoal.pl
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/fixseq
--- a/lib/Tools/fixseq	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/fixseq	Tue Jan 12 12:17:53 1999 +0100
@@ -32,4 +32,7 @@
 
 ## main
 
-find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixseq.pl
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixseq.pl
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/install
--- a/lib/Tools/install	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/install	Tue Jan 12 12:17:53 1999 +0100
@@ -61,8 +61,8 @@
 
 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
 
-BASH=$(type -path bash)
-[ -z "$BASH" ] && fail "Cannot find bash!"
+#set by configure
+AUTO_BASH=/bin/bash
 
 echo "using $DISTDIR"
 
@@ -71,7 +71,7 @@
   BIN="$BINDIR/$NAME"
   DIST="$DISTDIR/bin/$NAME"
   echo "installing $BIN"
-  echo "#!$BASH" >$BIN || fail "Cannot write file: $BIN"
+  echo "#!$AUTO_BASH" >$BIN || fail "Cannot write file: $BIN"
   echo >>$BIN
   echo "exec $DIST \"\$@\"" >>$BIN
   chmod +x $BIN
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/logo
--- a/lib/Tools/logo	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/logo	Tue Jan 12 12:17:53 1999 +0100
@@ -69,9 +69,12 @@
   OUTFILE="isabelle${OUTFILE}.eps"
 fi
 
+#set by configure
+AUTO_PERL=perl
+
 if [ "$OUTFILE" = "-" ]; then
-  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
+  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
 else
   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
-  perl -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
+  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
 fi
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/nonascii
--- a/lib/Tools/nonascii	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/nonascii	Tue Jan 12 12:17:53 1999 +0100
@@ -29,6 +29,9 @@
 
 ## main
 
+#set by configure
+AUTO_PERL=perl
+
 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
-  xargs perl -w -e \
+  xargs $AUTO_PERL -w -e \
     'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/symbolinput
--- a/lib/Tools/symbolinput	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/symbolinput	Tue Jan 12 12:17:53 1999 +0100
@@ -4,4 +4,7 @@
 #
 # DESCRIPTION: translate symbols into \<...> sequences
 
-exec perl -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
+#set by configure
+AUTO_PERL=perl
+
+exec $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/scripts/feeder
--- a/lib/scripts/feeder	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/scripts/feeder	Tue Jan 12 12:17:53 1999 +0100
@@ -79,4 +79,7 @@
 
 ## main
 
-exec perl -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
+#set by configure
+AUTO_PERL=perl
+
+exec $AUTO_PERL -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
diff -r aa97eb904692 -r 590f9e3bf4d8 lib/scripts/patch-scripts.bash
--- a/lib/scripts/patch-scripts.bash	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/scripts/patch-scripts.bash	Tue Jan 12 12:17:53 1999 +0100
@@ -38,7 +38,9 @@
 for FILE in $(find . -type f -print)
 do
   if [ -x "$FILE" ]; then
-    sed -e "s:^#!.*/bash:#!$BASH:" -e "s:^#!.*/perl:#!$PERL:" $FILE >$FILE~~
+    sed -e "s:^#!.*/bash:#!$BASH:" -e "s:^#!.*/perl:#!$PERL:" \
+      -e "s:^AUTO_BASH=.*/bash:AUTO_BASH=$BASH:" \
+      -e "s:^AUTO_PERL=.*/bash:AUTO_PERL=$PERL:" $FILE >$FILE~~
     if cmp -s $FILE $FILE~~; then
       rm $FILE~~
     else