# HG changeset patch
# User kleing
# Date 1024591711 -7200
# Node ID a2b09d99e5cfa3a856420b5a0344d23973c7ad4c
# Parent  52df43782fab97529db1ca326d12dc784b96100e
fail early

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