changeset 15847 | c05c7670f166 |
parent 15574 | b1d1b5bfc464 |
child 26576 | fc76b7b79ba9 |
15846:6f24b0c36dbd | 15847:c05c7670f166 |
---|---|
34 |
34 |
35 |
35 |
36 ## main |
36 ## main |
37 |
37 |
38 #set by configure |
38 #set by configure |
39 AUTO_PERL=/usr/bin/perl |
39 AUTO_PERL=perl |
40 |
40 |
41 find $SPECS \( -name \*.ML \) -print | \ |
41 find $SPECS \( -name \*.ML \) -print | \ |
42 xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl" |
42 xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl" |