equal
deleted
inserted
replaced
27 SPECS="$@"; shift $# |
27 SPECS="$@"; shift $# |
28 |
28 |
29 |
29 |
30 ## main |
30 ## main |
31 |
31 |
32 PERL=$(type -path perl) |
32 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \ |
33 if [ -z $PERL ]; then |
33 xargs perl -w -e \ |
34 echo "$PRG fatal error: no perl!?" |
34 'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}' |
35 else |
|
36 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \ |
|
37 xargs $PERL -e \ |
|
38 'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}' |
|
39 fi |
|