lib/Tools/makeall
author wenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01 ago)
changeset 9788 df671fa2562a
parent 7277 bb9502f9154a
child 10511 efb3428c9879
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2502
     2
#
wenzelm@2502
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2502
     6
#
wenzelm@4456
     7
# DESCRIPTION: apply make utility to all logics
wenzelm@2502
     8
wenzelm@4456
     9
## global settings
wenzelm@2502
    10
wenzelm@4456
    11
ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF"
wenzelm@2502
    12
wenzelm@2502
    13
wenzelm@4456
    14
## diagnostics
wenzelm@2502
    15
wenzelm@9788
    16
PRG=$(basename "$0")
wenzelm@2502
    17
wenzelm@4456
    18
function usage()
wenzelm@4456
    19
{
wenzelm@4456
    20
  echo
wenzelm@4456
    21
  echo "Usage: $PRG [ARGS ...]"
wenzelm@4456
    22
  echo
wenzelm@4456
    23
  echo "  Apply isatool make to all logics (passing ARGS)."
wenzelm@4456
    24
  echo
wenzelm@4456
    25
  exit 1
wenzelm@4456
    26
}
wenzelm@2502
    27
wenzelm@2502
    28
wenzelm@4456
    29
## main
wenzelm@4456
    30
wenzelm@4456
    31
[ "$1" = "-?" ] && usage
wenzelm@2502
    32
wenzelm@2502
    33
wenzelm@4456
    34
SECONDS=0
wenzelm@7277
    35
DATE=$(date)
wenzelm@7277
    36
HOST=$(hostname)
wenzelm@7277
    37
echo "Started at $DATE ($HOST)"
wenzelm@2502
    38
wenzelm@4456
    39
for L in $ALL_LOGICS
wenzelm@4456
    40
do
wenzelm@9788
    41
  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" )
wenzelm@4456
    42
done
wenzelm@2502
    43
wenzelm@4456
    44
echo -n "Finished at "; date
wenzelm@2502
    45
wenzelm@9788
    46
ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
wenzelm@4456
    47
echo "$ELAPSED total elapsed time"