diff -r 52df43782fab -r a2b09d99e5cf lib/Tools/makeall --- a/lib/Tools/makeall Thu Jun 20 18:23:58 2002 +0200 +++ b/lib/Tools/makeall Thu Jun 20 18:48:31 2002 +0200 @@ -25,6 +25,11 @@ exit 1 } +function fail() +{ + echo "$1" >&2 + exit 2 +} ## main @@ -34,7 +39,7 @@ for L in $ALL_LOGICS do - ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) + ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || fail "Logic $L failed!" done echo -n "Finished at "; date