| author | wenzelm | 
| Tue, 01 Aug 2000 00:19:07 +0200 | |
| changeset 9483 | 708a8a05497d | 
| parent 3007 | e5efa177ee0c | 
| child 9788 | df671fa2562a | 
| permissions | -rwxr-xr-x | 
#!/bin/bash # # $Id$ # # DESCRIPTION: collect heap names from ISABELLE_PATH PRG=$(basename $0) function usage() { echo echo "Usage: $PRG" echo echo " Collect heap file names from ISABELLE_PATH." echo exit 1 } ## main [ $# -ne 0 ] && usage LOGICS="" for DIR in $(echo $ISABELLE_PATH | tr : " ") do for FILE in $DIR/* do if [ -f "$FILE" ]; then NAME=$(basename "$FILE") LOGICS="$LOGICS $NAME" fi done done echo $({ for L in $LOGICS; do echo $L; done; } | sort | uniq)