# HG changeset patch
# User wenzelm
# Date 1342868251 -7200
# Node ID bb1d4ec90f3088e33602523e1fef1efe344df2be
# Parent  5787e1c911d0ada08e99f978a4d8510768867e01
tuned -- no dependency on exit function;

diff -r 5787e1c911d0 -r bb1d4ec90f30 src/Pure/build
--- a/src/Pure/build	Sat Jul 21 12:42:28 2012 +0200
+++ b/src/Pure/build	Sat Jul 21 12:57:31 2012 +0200
@@ -81,11 +81,11 @@
 if [ "$TARGET" = RAW ]; then
   if [ "$BUILD_IMAGES" = false ]; then
     "$ISABELLE_PROCESS" \
-      -e "use\"$COMPAT\" handle _ => exit 1;" \
+      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
   else
     "$ISABELLE_PROCESS" \
-      -e "use\"$COMPAT\" handle _ => exit 1;" \
+      -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -e "structure Isar = struct fun main () = () end;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
       -q -w RAW_ML_SYSTEM RAW
@@ -93,11 +93,11 @@
 else
   if [ "$BUILD_IMAGES" = false ]; then
     "$ISABELLE_PROCESS" \
-      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
   else
     "$ISABELLE_PROCESS" \
-      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
       -f -q -w RAW_ML_SYSTEM Pure
   fi