changeset 65948 | de7888573ed7 |
parent 65936 | aece72468de5 |
child 66048 | d244a895da50 |
--- a/src/Pure/Tools/build.ML Sat May 27 13:07:27 2017 +0200 +++ b/src/Pure/Tools/build.ML Sat May 27 13:20:35 2017 +0200 @@ -225,7 +225,7 @@ val _ = Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message build_session args - handle exn => (List.app (error_message o #2) (Runtime.exn_messages exn); Exn.reraise exn); + handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn); val _ = Options.reset_default (); in () end;