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