src/Pure/System/build.ML
changeset 48662 b171bcd5dd86
parent 48634 30a6e841390a
child 48672 9bc7922ba2ae
--- a/src/Pure/System/build.ML	Fri Aug 03 14:52:45 2012 +0200
+++ b/src/Pure/System/build.ML	Fri Aug 03 16:00:12 2012 +0200
@@ -79,7 +79,9 @@
     val _ = Session.finish ();
     val _ = if do_output then () else quit ();
   in () end
-  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
+  handle exn =>
+    (Output.error_msg (ML_Compiler.exn_message exn);
+     if Exn.is_interrupt exn then exit 130 else exit 1);
 
 end;