lib/Tools/nonascii
changeset 6082 590f9e3bf4d8
parent 4508 f102cb0140fe
child 9788 df671fa2562a
equal deleted inserted replaced
6081:aa97eb904692 6082:590f9e3bf4d8
    27 SPECS="$@"; shift $#
    27 SPECS="$@"; shift $#
    28 
    28 
    29 
    29 
    30 ## main
    30 ## main
    31 
    31 
       
    32 #set by configure
       
    33 AUTO_PERL=perl
       
    34 
    32 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
    35 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
    33   xargs perl -w -e \
    36   xargs $AUTO_PERL -w -e \
    34     'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
    37     'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'