lib/Tools/fixclasimp
changeset 6082 590f9e3bf4d8
parent 4508 f102cb0140fe
child 9788 df671fa2562a
equal deleted inserted replaced
6081:aa97eb904692 6082:590f9e3bf4d8
    30 SPECS="$@"; shift $#
    30 SPECS="$@"; shift $#
    31 
    31 
    32 
    32 
    33 ## main
    33 ## main
    34 
    34 
    35 find $SPECS -name \*.ML -print | xargs perl -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl
    35 #set by configure
       
    36 AUTO_PERL=perl
       
    37 
       
    38 find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl