| 10555 |      1 | #!/usr/bin/env bash
 | 
| 2333 |      2 | #
 | 
|  |      3 | # $Id$
 | 
| 9788 |      4 | # Author: Markus Wenzel, TU Muenchen
 | 
|  |      5 | # License: GPL (GNU GENERAL PUBLIC LICENSE)
 | 
| 2333 |      6 | #
 | 
|  |      7 | # DESCRIPTION: collect heap names from ISABELLE_PATH
 | 
|  |      8 | 
 | 
|  |      9 | 
 | 
| 9788 |     10 | PRG=$(basename "$0")
 | 
| 2333 |     11 | 
 | 
|  |     12 | function usage()
 | 
|  |     13 | {
 | 
|  |     14 |   echo
 | 
|  |     15 |   echo "Usage: $PRG"
 | 
|  |     16 |   echo
 | 
|  |     17 |   echo "  Collect heap file names from ISABELLE_PATH."
 | 
|  |     18 |   echo
 | 
|  |     19 |   exit 1
 | 
|  |     20 | }
 | 
|  |     21 | 
 | 
|  |     22 | 
 | 
|  |     23 | ## main
 | 
|  |     24 | 
 | 
| 9788 |     25 | [ "$#" -ne 0 ] && usage
 | 
| 2333 |     26 | 
 | 
|  |     27 | 
 | 
|  |     28 | LOGICS=""
 | 
|  |     29 | 
 | 
| 9788 |     30 | ORIG_IFS="$IFS"
 | 
|  |     31 | IFS=":"
 | 
|  |     32 | for DIR in $ISABELLE_PATH
 | 
| 2333 |     33 | do
 | 
| 9788 |     34 |   DIR="$DIR/$ML_IDENTIFIER"
 | 
|  |     35 |   for FILE in "$DIR"/*
 | 
| 2333 |     36 |   do
 | 
|  |     37 |     if [ -f "$FILE" ]; then
 | 
|  |     38 |       NAME=$(basename "$FILE")
 | 
|  |     39 |       LOGICS="$LOGICS $NAME"
 | 
|  |     40 |     fi
 | 
|  |     41 |   done
 | 
|  |     42 | done
 | 
| 9788 |     43 | IFS="$ORIG_IFS"
 | 
| 2333 |     44 | 
 | 
| 9788 |     45 | echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)
 |