author | wenzelm |
Thu, 17 Apr 1997 10:30:57 +0200 | |
changeset 2968 | 8ba30b031f31 |
parent 2936 | bd33e7aae062 |
child 3007 | e5efa177ee0c |
permissions | -rwxr-xr-x |
#!/bin/bash -norc # # $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)