diff -r 5f454603228b -r 5c0a2583f997 Admin/build
--- a/Admin/build	Sat Jan 09 16:31:19 2010 +0100
+++ b/Admin/build	Sat Jan 09 18:22:40 2010 +0100
@@ -59,7 +59,7 @@
 function build_browser ()
 {
   pushd "$ISABELLE_HOME/lib/browser" >/dev/null
-  "$ISABELLE_TOOL" env ./build || fail "Failed!"
+  "$ISABELLE_TOOL" env ./build || exit $?
   popd >/dev/null
 }
 
@@ -84,7 +84,7 @@
 function build_jars ()
 {
   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
-  "$ISABELLE_TOOL" env ./build-jars || fail "Failed!"
+  "$ISABELLE_TOOL" env ./build-jars || exit $?
   popd >/dev/null
 }