| author | wenzelm | 
| Tue, 01 Aug 2000 00:19:07 +0200 | |
| changeset 9483 | 708a8a05497d | 
| parent 3007 | e5efa177ee0c | 
| child 9788 | df671fa2562a | 
| permissions | -rwxr-xr-x | 
| 3007 | 1 | #!/bin/bash | 
| 2333 | 2 | # | 
| 3 | # $Id$ | |
| 4 | # | |
| 5 | # DESCRIPTION: collect heap names from ISABELLE_PATH | |
| 6 | ||
| 7 | ||
| 8 | PRG=$(basename $0) | |
| 9 | ||
| 10 | function usage() | |
| 11 | {
 | |
| 12 | echo | |
| 13 | echo "Usage: $PRG" | |
| 14 | echo | |
| 15 | echo " Collect heap file names from ISABELLE_PATH." | |
| 16 | echo | |
| 17 | exit 1 | |
| 18 | } | |
| 19 | ||
| 20 | ||
| 21 | ## main | |
| 22 | ||
| 23 | [ $# -ne 0 ] && usage | |
| 24 | ||
| 25 | ||
| 26 | LOGICS="" | |
| 27 | ||
| 28 | for DIR in $(echo $ISABELLE_PATH | tr : " ") | |
| 29 | do | |
| 2968 | 30 | for FILE in $DIR/* | 
| 2333 | 31 | do | 
| 32 | if [ -f "$FILE" ]; then | |
| 33 | NAME=$(basename "$FILE") | |
| 34 | LOGICS="$LOGICS $NAME" | |
| 35 | fi | |
| 36 | done | |
| 37 | done | |
| 38 | ||
| 2936 
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
 wenzelm parents: 
2591diff
changeset | 39 | echo $({ for L in $LOGICS; do echo $L; done; } | sort | uniq)
 |