diff -r 8139edae3bf5 -r c26fc3baeffc lib/Tools/makeall --- a/lib/Tools/makeall Thu Jun 20 22:30:00 2002 +0200 +++ b/lib/Tools/makeall Fri Jun 21 12:35:33 2002 +0200 @@ -35,14 +35,18 @@ [ "$1" = "-?" ] && usage +FAIL="" + echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" for L in $ALL_LOGICS do - ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || fail "Logic $L failed!" + ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L " done echo -n "Finished at "; date ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") echo "$ELAPSED total elapsed time" + +[ "$FAIL" == "" ] || fail "Logics ${FAIL}FAILED!"