# HG changeset patch
# User wenzelm
# Date 1344422020 -7200
# Node ID a45ba78abcc1e901f3589a37d2d661253ade48ec
# Parent  519b6e53179b33446f0d26e9b81ee5114694aab9
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;

diff -r 519b6e53179b -r a45ba78abcc1 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Wed Aug 08 12:13:34 2012 +0200
+++ b/src/Pure/System/build.ML	Wed Aug 08 12:33:40 2012 +0200
@@ -6,7 +6,7 @@
 
 signature BUILD =
 sig
-  val build: string -> 'a
+  val build: string -> unit
 end;
 
 structure Build: BUILD =
diff -r 519b6e53179b -r a45ba78abcc1 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Wed Aug 08 12:13:34 2012 +0200
+++ b/src/Pure/System/command_line.ML	Wed Aug 08 12:33:40 2012 +0200
@@ -6,7 +6,7 @@
 
 signature COMMAND_LINE =
 sig
-  val tool: (unit -> int) -> 'a
+  val tool: (unit -> int) -> unit
 end;
 
 structure Command_Line: COMMAND_LINE =
@@ -17,7 +17,7 @@
     let val rc =
       restore_attributes body () handle exn =>
         (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
-    in exit rc; raise Fail "ERROR" end) ();
+    in if rc = 0 then () else exit rc end) ();
 
 end;