diff -r 9149ebdd0241 -r b171bcd5dd86 src/Pure/build --- a/src/Pure/build Fri Aug 03 14:52:45 2012 +0200 +++ b/src/Pure/build Fri Aug 03 16:00:12 2012 +0200 @@ -61,11 +61,11 @@ if [ "$TARGET" = RAW ]; then if [ -z "$OUTPUT" ]; then "$ISABELLE_PROCESS" \ - -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ + -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \ -q RAW_ML_SYSTEM else "$ISABELLE_PROCESS" \ - -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ + -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \ -e "structure Isar = struct fun main () = () end;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ -q -w RAW_ML_SYSTEM "$OUTPUT" @@ -73,11 +73,11 @@ else if [ -z "$OUTPUT" ]; then "$ISABELLE_PROCESS" \ - -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \ -q RAW_ML_SYSTEM else "$ISABELLE_PROCESS" \ - -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ -f -q -w RAW_ML_SYSTEM "$OUTPUT" fi