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;