author | paulson |
Wed, 19 Aug 1998 10:29:01 +0200 | |
changeset 5339 | 22c195854229 |
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)