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