lib/Tools/findlogics
author wenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01)
changeset 9788 df671fa2562a
parent 3007 e5efa177ee0c
child 10555 2323ec838401
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2333
     2
#
wenzelm@2333
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2333
     6
#
wenzelm@2333
     7
# DESCRIPTION: collect heap names from ISABELLE_PATH
wenzelm@2333
     8
wenzelm@2333
     9
wenzelm@9788
    10
PRG=$(basename "$0")
wenzelm@2333
    11
wenzelm@2333
    12
function usage()
wenzelm@2333
    13
{
wenzelm@2333
    14
  echo
wenzelm@2333
    15
  echo "Usage: $PRG"
wenzelm@2333
    16
  echo
wenzelm@2333
    17
  echo "  Collect heap file names from ISABELLE_PATH."
wenzelm@2333
    18
  echo
wenzelm@2333
    19
  exit 1
wenzelm@2333
    20
}
wenzelm@2333
    21
wenzelm@2333
    22
wenzelm@2333
    23
## main
wenzelm@2333
    24
wenzelm@9788
    25
[ "$#" -ne 0 ] && usage
wenzelm@2333
    26
wenzelm@2333
    27
wenzelm@2333
    28
LOGICS=""
wenzelm@2333
    29
wenzelm@9788
    30
ORIG_IFS="$IFS"
wenzelm@9788
    31
IFS=":"
wenzelm@9788
    32
for DIR in $ISABELLE_PATH
wenzelm@2333
    33
do
wenzelm@9788
    34
  DIR="$DIR/$ML_IDENTIFIER"
wenzelm@9788
    35
  for FILE in "$DIR"/*
wenzelm@2333
    36
  do
wenzelm@2333
    37
    if [ -f "$FILE" ]; then
wenzelm@2333
    38
      NAME=$(basename "$FILE")
wenzelm@2333
    39
      LOGICS="$LOGICS $NAME"
wenzelm@2333
    40
    fi
wenzelm@2333
    41
  done
wenzelm@2333
    42
done
wenzelm@9788
    43
IFS="$ORIG_IFS"
wenzelm@2333
    44
wenzelm@9788
    45
echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)