# HG changeset patch
# User wenzelm
# Date 883743893 -3600
# Node ID f102cb0140fe74f3f7e37c494faec25d02fa0cb7
# Parent  f313d8fb8f49034317175e6b6a1dd76147f7e372
do require perl;

diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/expandshort
--- a/lib/Tools/expandshort	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/expandshort	Fri Jan 02 13:24:53 1998 +0100
@@ -32,9 +32,4 @@
 
 ## main
 
-PERL=$(type -path perl)
-if [ -z $PERL ]; then
-  echo "$PRG fatal error: no perl!?"
-else
-  find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/expandshort.pl
-fi
+find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/expandshort.pl
diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/fixclasimp
--- a/lib/Tools/fixclasimp	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/fixclasimp	Fri Jan 02 13:24:53 1998 +0100
@@ -32,9 +32,4 @@
 
 ## main
 
-PERL=$(type -path perl)
-if [ -z $PERL ]; then
-  echo "$PRG fatal error: no perl!?"
-else
-  find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/fixclasimp.pl
-fi
+find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl
diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/fixdots
--- a/lib/Tools/fixdots	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/fixdots	Fri Jan 02 13:24:53 1998 +0100
@@ -32,10 +32,5 @@
 
 ## main
 
-PERL=$(type -path perl)
-if [ -z $PERL ]; then
-  echo "$PRG fatal error: no perl!?"
-else
-  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
-    xargs $PERL $ISABELLE_HOME/lib/scripts/fixdots.pl
-fi
+find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
+  xargs perl -w $ISABELLE_HOME/lib/scripts/fixdots.pl
diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/fixseq
--- a/lib/Tools/fixseq	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/fixseq	Fri Jan 02 13:24:53 1998 +0100
@@ -32,9 +32,4 @@
 
 ## main
 
-PERL=$(type -path perl)
-if [ -z $PERL ]; then
-  echo "$PRG fatal error: no perl!?"
-else
-  find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/fixseq.pl
-fi
+find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixseq.pl
diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/nonascii
--- a/lib/Tools/nonascii	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/nonascii	Fri Jan 02 13:24:53 1998 +0100
@@ -29,11 +29,6 @@
 
 ## main
 
-PERL=$(type -path perl)
-if [ -z $PERL ]; then
-  echo "$PRG fatal error: no perl!?"
-else
-  find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
-    xargs $PERL -e \
-      'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
-fi
+find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
+  xargs perl -w -e \
+    'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
diff -r f313d8fb8f49 -r f102cb0140fe lib/Tools/symbolinput
--- a/lib/Tools/symbolinput	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/Tools/symbolinput	Fri Jan 02 13:24:53 1998 +0100
@@ -3,15 +3,5 @@
 # $Id$
 #
 # DESCRIPTION: translate symbols into \<...> sequences
-#
-# NOTE: If perl is unavailable we simply fall back on ucat!
 
-
-PERL=$(type -path perl)
-
-if [ -z "$PERL" ]
-then
-  exec $ISABELLE_HOME/lib/scripts/ucat "$@"
-else
-  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
-fi
+exec perl -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
diff -r f313d8fb8f49 -r f102cb0140fe lib/scripts/patch-scripts.bash
--- a/lib/scripts/patch-scripts.bash	Fri Jan 02 11:59:06 1998 +0100
+++ b/lib/scripts/patch-scripts.bash	Fri Jan 02 13:24:53 1998 +0100
@@ -23,7 +23,7 @@
     echo "$DEFAULT"
     return
   else
-    echo "WARNING: $BASE not found!" >&2
+    echo "ERROR: $BASE not found!" >&2
     echo "$DEFAULT"
     return
   fi