do require perl;
authorwenzelm
Fri Jan 02 13:24:53 1998 +0100 (1998-01-02)
changeset 4508f102cb0140fe
parent 4507 f313d8fb8f49
child 4509 828148415197
do require perl;
lib/Tools/expandshort
lib/Tools/fixclasimp
lib/Tools/fixdots
lib/Tools/fixseq
lib/Tools/nonascii
lib/Tools/symbolinput
lib/scripts/patch-scripts.bash
     1.1 --- a/lib/Tools/expandshort	Fri Jan 02 11:59:06 1998 +0100
     1.2 +++ b/lib/Tools/expandshort	Fri Jan 02 13:24:53 1998 +0100
     1.3 @@ -32,9 +32,4 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -PERL=$(type -path perl)
     1.8 -if [ -z $PERL ]; then
     1.9 -  echo "$PRG fatal error: no perl!?"
    1.10 -else
    1.11 -  find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/expandshort.pl
    1.12 -fi
    1.13 +find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/expandshort.pl
     2.1 --- a/lib/Tools/fixclasimp	Fri Jan 02 11:59:06 1998 +0100
     2.2 +++ b/lib/Tools/fixclasimp	Fri Jan 02 13:24:53 1998 +0100
     2.3 @@ -32,9 +32,4 @@
     2.4  
     2.5  ## main
     2.6  
     2.7 -PERL=$(type -path perl)
     2.8 -if [ -z $PERL ]; then
     2.9 -  echo "$PRG fatal error: no perl!?"
    2.10 -else
    2.11 -  find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/fixclasimp.pl
    2.12 -fi
    2.13 +find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl
     3.1 --- a/lib/Tools/fixdots	Fri Jan 02 11:59:06 1998 +0100
     3.2 +++ b/lib/Tools/fixdots	Fri Jan 02 13:24:53 1998 +0100
     3.3 @@ -32,10 +32,5 @@
     3.4  
     3.5  ## main
     3.6  
     3.7 -PERL=$(type -path perl)
     3.8 -if [ -z $PERL ]; then
     3.9 -  echo "$PRG fatal error: no perl!?"
    3.10 -else
    3.11 -  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    3.12 -    xargs $PERL $ISABELLE_HOME/lib/scripts/fixdots.pl
    3.13 -fi
    3.14 +find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    3.15 +  xargs perl -w $ISABELLE_HOME/lib/scripts/fixdots.pl
     4.1 --- a/lib/Tools/fixseq	Fri Jan 02 11:59:06 1998 +0100
     4.2 +++ b/lib/Tools/fixseq	Fri Jan 02 13:24:53 1998 +0100
     4.3 @@ -32,9 +32,4 @@
     4.4  
     4.5  ## main
     4.6  
     4.7 -PERL=$(type -path perl)
     4.8 -if [ -z $PERL ]; then
     4.9 -  echo "$PRG fatal error: no perl!?"
    4.10 -else
    4.11 -  find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/fixseq.pl
    4.12 -fi
    4.13 +find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixseq.pl
     5.1 --- a/lib/Tools/nonascii	Fri Jan 02 11:59:06 1998 +0100
     5.2 +++ b/lib/Tools/nonascii	Fri Jan 02 13:24:53 1998 +0100
     5.3 @@ -29,11 +29,6 @@
     5.4  
     5.5  ## main
     5.6  
     5.7 -PERL=$(type -path perl)
     5.8 -if [ -z $PERL ]; then
     5.9 -  echo "$PRG fatal error: no perl!?"
    5.10 -else
    5.11 -  find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
    5.12 -    xargs $PERL -e \
    5.13 -      'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
    5.14 -fi
    5.15 +find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
    5.16 +  xargs perl -w -e \
    5.17 +    'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
     6.1 --- a/lib/Tools/symbolinput	Fri Jan 02 11:59:06 1998 +0100
     6.2 +++ b/lib/Tools/symbolinput	Fri Jan 02 13:24:53 1998 +0100
     6.3 @@ -3,15 +3,5 @@
     6.4  # $Id$
     6.5  #
     6.6  # DESCRIPTION: translate symbols into \<...> sequences
     6.7 -#
     6.8 -# NOTE: If perl is unavailable we simply fall back on ucat!
     6.9  
    6.10 -
    6.11 -PERL=$(type -path perl)
    6.12 -
    6.13 -if [ -z "$PERL" ]
    6.14 -then
    6.15 -  exec $ISABELLE_HOME/lib/scripts/ucat "$@"
    6.16 -else
    6.17 -  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
    6.18 -fi
    6.19 +exec perl -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
     7.1 --- a/lib/scripts/patch-scripts.bash	Fri Jan 02 11:59:06 1998 +0100
     7.2 +++ b/lib/scripts/patch-scripts.bash	Fri Jan 02 13:24:53 1998 +0100
     7.3 @@ -23,7 +23,7 @@
     7.4      echo "$DEFAULT"
     7.5      return
     7.6    else
     7.7 -    echo "WARNING: $BASE not found!" >&2
     7.8 +    echo "ERROR: $BASE not found!" >&2
     7.9      echo "$DEFAULT"
    7.10      return
    7.11    fi