author | wenzelm |
Tue, 28 Jul 1998 17:02:41 +0200 | |
changeset 5208 | cea0adbc7276 |
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)