wenzelm@2333: #!/bin/bash -norc wenzelm@2333: # wenzelm@2333: # $Id$ wenzelm@2333: # wenzelm@2333: # DESCRIPTION: collect heap names from ISABELLE_PATH wenzelm@2333: wenzelm@2333: wenzelm@2333: PRG=$(basename $0) wenzelm@2333: wenzelm@2333: function usage() wenzelm@2333: { wenzelm@2333: echo wenzelm@2333: echo "Usage: $PRG" wenzelm@2333: echo wenzelm@2333: echo " Collect heap file names from ISABELLE_PATH." wenzelm@2333: echo wenzelm@2333: exit 1 wenzelm@2333: } wenzelm@2333: wenzelm@2333: wenzelm@2333: ## main wenzelm@2333: wenzelm@2333: [ $# -ne 0 ] && usage wenzelm@2333: wenzelm@2333: wenzelm@2333: LOGICS="" wenzelm@2333: wenzelm@2333: for DIR in $(echo $ISABELLE_PATH | tr : " ") wenzelm@2333: do wenzelm@2968: for FILE in $DIR/* wenzelm@2333: do wenzelm@2333: if [ -f "$FILE" ]; then wenzelm@2333: NAME=$(basename "$FILE") wenzelm@2333: LOGICS="$LOGICS $NAME" wenzelm@2333: fi wenzelm@2333: done wenzelm@2333: done wenzelm@2333: wenzelm@2936: echo $({ for L in $LOGICS; do echo $L; done; } | sort | uniq)