equal
deleted
inserted
replaced
23 echo " Apply isatool make to all logics (passing ARGS)." |
23 echo " Apply isatool make to all logics (passing ARGS)." |
24 echo |
24 echo |
25 exit 1 |
25 exit 1 |
26 } |
26 } |
27 |
27 |
|
28 function fail() |
|
29 { |
|
30 echo "$1" >&2 |
|
31 exit 2 |
|
32 } |
28 |
33 |
29 ## main |
34 ## main |
30 |
35 |
31 [ "$1" = "-?" ] && usage |
36 [ "$1" = "-?" ] && usage |
32 |
37 |
33 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
38 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
34 |
39 |
35 for L in $ALL_LOGICS |
40 for L in $ALL_LOGICS |
36 do |
41 do |
37 ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) |
42 ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || fail "Logic $L failed!" |
38 done |
43 done |
39 |
44 |
40 echo -n "Finished at "; date |
45 echo -n "Finished at "; date |
41 |
46 |
42 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") |
47 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") |