--- 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
--- 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
--- 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
--- 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
--- 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: $_"; }}'
--- 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 "$@"
--- 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