changeset 56303 | 4cc3f4db3447 |
parent 54387 | 890e983cb07b |
child 56628 | a2df9de46060 |
--- a/src/Pure/System/command_line.ML Thu Mar 27 13:00:40 2014 +0100 +++ b/src/Pure/System/command_line.ML Thu Mar 27 17:12:40 2014 +0100 @@ -19,7 +19,7 @@ restore_attributes body () handle exn => let val _ = - ML_Compiler.exn_error_message exn + Runtime.exn_error_message exn handle _ => Output.error_message "Exception raised, but failed to print details!"; in if Exn.is_interrupt exn then 130 else 1 end; in if rc = 0 then () else exit rc end) ();