changeset 26576 | fc76b7b79ba9 |
parent 15847 | c05c7670f166 |
26575:042617a1c86c | 26576:fc76b7b79ba9 |
---|---|
33 SPECS="$@"; shift "$#" |
33 SPECS="$@"; shift "$#" |
34 |
34 |
35 |
35 |
36 ## main |
36 ## main |
37 |
37 |
38 #set by configure |
|
39 AUTO_PERL=perl |
|
40 |
|
41 find $SPECS \( -name \*.ML \) -print | \ |
38 find $SPECS \( -name \*.ML \) -print | \ |
42 xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl" |
39 xargs perl -w "$ISABELLE_HOME/lib/scripts/convert.pl" |