equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 # |
6 # |
5 # DESCRIPTION: fix references to implicit claset and simpset |
7 # DESCRIPTION: fix references to implicit claset and simpset |
6 |
8 |
7 |
9 |
8 ## diagnostics |
10 ## diagnostics |
9 |
11 |
10 PRG=$(basename $0) |
12 PRG=$(basename "$0") |
11 |
13 |
12 function usage() |
14 function usage() |
13 { |
15 { |
14 echo |
16 echo |
15 echo "Usage: $PRG [FILES|DIRS...]" |
17 echo "Usage: $PRG [FILES|DIRS...]" |
23 } |
25 } |
24 |
26 |
25 |
27 |
26 ## process command line |
28 ## process command line |
27 |
29 |
28 [ $# -eq 0 -o "$1" = "-?" ] && usage |
30 [ "$#" -eq 0 -o "$1" = "-?" ] && usage |
29 |
31 |
30 SPECS="$@"; shift $# |
32 SPECS="$@"; shift "$#" |
31 |
33 |
32 |
34 |
33 ## main |
35 ## main |
34 |
36 |
35 #set by configure |
37 #set by configure |
36 AUTO_PERL=perl |
38 AUTO_PERL=perl |
37 |
39 |
38 find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl |
40 find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl" |