| changeset 4508 | f102cb0140fe |
| parent 4416 | c32a5c724263 |
| child 6082 | 590f9e3bf4d8 |
| 4507:f313d8fb8f49 | 4508:f102cb0140fe |
|---|---|
30 SPECS="$@"; shift $# |
30 SPECS="$@"; shift $# |
31 |
31 |
32 |
32 |
33 ## main |
33 ## main |
34 |
34 |
35 PERL=$(type -path perl) |
35 find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/expandshort.pl |
36 if [ -z $PERL ]; then |
|
37 echo "$PRG fatal error: no perl!?" |
|
38 else |
|
39 find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/expandshort.pl |
|
40 fi |