author | wenzelm |
Thu, 26 Nov 2020 16:19:55 +0100 | |
changeset 72725 | 27d9aa2a4010 |
parent 72724 | 75cce7926ec1 |
child 72726 | ec6a27bbdab8 |
--- a/src/Pure/Tools/build_job.scala Thu Nov 26 16:14:16 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Thu Nov 26 16:19:55 2020 +0100 @@ -167,6 +167,7 @@ export_consumer(session_name, args, Bytes(YXML.string_of_body(xml))) } export(Export.MARKUP, snapshot.xml_markup()) + export(Export.MESSAGES, snapshot.messages.map(_._1)) } session.all_messages += Session.Consumer[Any]("build_session_output")