| changeset 6082 | 590f9e3bf4d8 |
| parent 4508 | f102cb0140fe |
| child 9788 | df671fa2562a |
| 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: $_"; }}' |