more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
authorwenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48730 519b6e53179b
child 48732 f04320479ff9
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
src/Pure/System/build.ML
src/Pure/System/command_line.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 =
--- 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;