more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
--- 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 =
--- 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;