equal
deleted
inserted
replaced
33 |
33 |
34 |
34 |
35 ## main |
35 ## main |
36 |
36 |
37 #set by configure |
37 #set by configure |
38 AUTO_PERL=perl |
38 AUTO_PERL=/usr/bin/perl |
39 |
39 |
40 find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" |
40 find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" |
41 find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" |
41 find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl" |