| author | skalberg | 
| Tue, 21 Oct 2003 11:09:23 +0200 | |
| changeset 14242 | ec70653a02bf | 
| parent 13834 | 4d50cf8ea3d7 | 
| child 14281 | a8c4a1e63071 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1 | #!/usr/bin/env bash | 
| 2502 | 2 | # | 
| 3 | # $Id$ | |
| 9788 | 4 | # Author: Markus Wenzel, TU Muenchen | 
| 5 | # License: GPL (GNU GENERAL PUBLIC LICENSE) | |
| 2502 | 6 | # | 
| 4456 | 7 | # DESCRIPTION: apply make utility to all logics | 
| 2502 | 8 | |
| 4456 | 9 | ## global settings | 
| 2502 | 10 | |
| 4456 | 11 | ALL_LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Pure Sequents ZF" | 
| 2502 | 12 | |
| 13 | ||
| 4456 | 14 | ## diagnostics | 
| 2502 | 15 | |
| 10511 | 16 | PRG="$(basename "$0")" | 
| 2502 | 17 | |
| 4456 | 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 | } | |
| 2502 | 27 | |
| 13229 | 28 | function fail() | 
| 29 | {
 | |
| 30 | echo "$1" >&2 | |
| 31 | exit 2 | |
| 32 | } | |
| 2502 | 33 | |
| 4456 | 34 | ## main | 
| 35 | ||
| 36 | [ "$1" = "-?" ] && usage | |
| 2502 | 37 | |
| 13235 
c26fc3baeffc
fail not so early, but produce correct exit code in the end
 kleing parents: 
13229diff
changeset | 38 | FAIL="" | 
| 
c26fc3baeffc
fail not so early, but produce correct exit code in the end
 kleing parents: 
13229diff
changeset | 39 | |
| 10511 | 40 | echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" | 
| 2502 | 41 | |
| 4456 | 42 | for L in $ALL_LOGICS | 
| 43 | do | |
| 13235 
c26fc3baeffc
fail not so early, but produce correct exit code in the end
 kleing parents: 
13229diff
changeset | 44 | ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L " | 
| 4456 | 45 | done | 
| 2502 | 46 | |
| 4456 | 47 | echo -n "Finished at "; date | 
| 2502 | 48 | |
| 9788 | 49 | ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
 | 
| 4456 | 50 | echo "$ELAPSED total elapsed time" | 
| 13235 
c26fc3baeffc
fail not so early, but produce correct exit code in the end
 kleing parents: 
13229diff
changeset | 51 | |
| 13834 | 52 | [ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"
 |