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: collect heap names from ISABELLE_PATH |
7 # DESCRIPTION: collect heap names from ISABELLE_PATH |
6 |
8 |
7 |
9 |
8 PRG=$(basename $0) |
10 PRG=$(basename "$0") |
9 |
11 |
10 function usage() |
12 function usage() |
11 { |
13 { |
12 echo |
14 echo |
13 echo "Usage: $PRG" |
15 echo "Usage: $PRG" |
18 } |
20 } |
19 |
21 |
20 |
22 |
21 ## main |
23 ## main |
22 |
24 |
23 [ $# -ne 0 ] && usage |
25 [ "$#" -ne 0 ] && usage |
24 |
26 |
25 |
27 |
26 LOGICS="" |
28 LOGICS="" |
27 |
29 |
28 for DIR in $(echo $ISABELLE_PATH | tr : " ") |
30 ORIG_IFS="$IFS" |
|
31 IFS=":" |
|
32 for DIR in $ISABELLE_PATH |
29 do |
33 do |
30 for FILE in $DIR/* |
34 DIR="$DIR/$ML_IDENTIFIER" |
|
35 for FILE in "$DIR"/* |
31 do |
36 do |
32 if [ -f "$FILE" ]; then |
37 if [ -f "$FILE" ]; then |
33 NAME=$(basename "$FILE") |
38 NAME=$(basename "$FILE") |
34 LOGICS="$LOGICS $NAME" |
39 LOGICS="$LOGICS $NAME" |
35 fi |
40 fi |
36 done |
41 done |
37 done |
42 done |
|
43 IFS="$ORIG_IFS" |
38 |
44 |
39 echo $({ for L in $LOGICS; do echo $L; done; } | sort | uniq) |
45 echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq) |