author | wenzelm |
Fri, 07 Mar 1997 11:48:46 +0100 | |
changeset 2754 | 59bd96046ad6 |
parent 2591 | ae16f162f973 |
child 2936 | bd33e7aae062 |
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/$ML_SYSTEM-$PLATFORM/* 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)