# HG changeset patch
# User wenzelm
# Date 1207662430 -7200
# Node ID fc76b7b79ba9e50236ad1cd809e7caa0436c5b70
# Parent  042617a1c86cdd58e98330455ed2cce39ef4ae8a
removed obsolete AUTO_PERL feature;

diff -r 042617a1c86c -r fc76b7b79ba9 lib/Tools/convert
--- a/lib/Tools/convert	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/Tools/convert	Tue Apr 08 15:47:10 2008 +0200
@@ -35,8 +35,5 @@
 
 ## main
 
-#set by configure
-AUTO_PERL=perl
-
 find $SPECS \( -name \*.ML \) -print | \
-  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl"
+  xargs perl -w "$ISABELLE_HOME/lib/scripts/convert.pl"
diff -r 042617a1c86c -r fc76b7b79ba9 lib/Tools/dimacs2hol
--- a/lib/Tools/dimacs2hol	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/Tools/dimacs2hol	Tue Apr 08 15:47:10 2008 +0200
@@ -45,7 +45,4 @@
 
 ## main
 
-#set by configure
-AUTO_PERL=perl
-
-"$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@"
+exec perl -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@"
diff -r 042617a1c86c -r fc76b7b79ba9 lib/Tools/fixheaders
--- a/lib/Tools/fixheaders	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/Tools/fixheaders	Tue Apr 08 15:47:10 2008 +0200
@@ -33,8 +33,5 @@
 
 ## main
 
-#set by configure
-AUTO_PERL=perl
-
 find $SPECS -name \*.thy -print | \
-  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl"
+  xargs perl -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl"
diff -r 042617a1c86c -r fc76b7b79ba9 lib/Tools/keywords
--- a/lib/Tools/keywords	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/Tools/keywords	Tue Apr 08 15:47:10 2008 +0200
@@ -57,9 +57,6 @@
 
 ## main
 
-#set by configure
-AUTO_PERL=perl
-
 SESSIONS=""
 for LOG in $LOGS
 do
@@ -80,4 +77,4 @@
   fi
   echo
 done | \
-"$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"
+perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"
diff -r 042617a1c86c -r fc76b7b79ba9 lib/Tools/latex
--- a/lib/Tools/latex	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/Tools/latex	Tue Apr 08 15:47:10 2008 +0200
@@ -72,9 +72,6 @@
 
 # operations
 
-#set by configure
-AUTO_PERL=perl
-
 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
@@ -86,16 +83,16 @@
   for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
   do
     TARGET="$DIR"/$(basename "$STYLEFILE")
-    "$AUTO_PERL" -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
+    perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
   done
 }
 
 function extract_syms ()
 {
-  "$AUTO_PERL" -n \
+  perl -n \
     -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
     "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
-  "$AUTO_PERL" -n \
+  perl -n \
     -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
     "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
 }
diff -r 042617a1c86c -r fc76b7b79ba9 lib/Tools/logo
--- a/lib/Tools/logo	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/Tools/logo	Tue Apr 08 15:47:10 2008 +0200
@@ -70,12 +70,9 @@
   OUTFILE="isabelle${OUTFILE}.eps"
 fi
 
-#set by configure
-AUTO_PERL=perl
-
 if [ "$OUTFILE" = "-" ]; then
-  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
+  perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
 else
   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
-  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
+  perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
 fi
diff -r 042617a1c86c -r fc76b7b79ba9 lib/Tools/unsymbolize
--- a/lib/Tools/unsymbolize	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/Tools/unsymbolize	Tue Apr 08 15:47:10 2008 +0200
@@ -34,8 +34,5 @@
 
 ## main
 
-#set by configure
-AUTO_PERL=perl
-
 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
-  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
+  xargs perl -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
diff -r 042617a1c86c -r fc76b7b79ba9 lib/scripts/feeder
--- a/lib/scripts/feeder	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/scripts/feeder	Tue Apr 08 15:47:10 2008 +0200
@@ -75,7 +75,4 @@
 
 ## main
 
-#set by configure
-AUTO_PERL=perl
-
-exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"
+exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"
diff -r 042617a1c86c -r fc76b7b79ba9 lib/scripts/timestart.bash
--- a/lib/scripts/timestart.bash	Tue Apr 08 15:47:05 2008 +0200
+++ b/lib/scripts/timestart.bash	Tue Apr 08 15:47:10 2008 +0200
@@ -7,13 +7,10 @@
 
 TIMES_RESULT=""
 
-#set by configure
-AUTO_PERL=perl
-
 function get_times () {
   local TMP="/tmp/get_times$$"
   times > "$TMP"   # No pipe here!
-  TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | "$AUTO_PERL" -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
+  TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | perl -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
   rm -f "$TMP"
 }