# HG changeset patch
# User wenzelm
# Date 1606403995 -3600
# Node ID 27d9aa2a401046fc1b12903fa7c495d6d4ce192b
# Parent  75cce7926ec16f65c0fa05c814df9571ca7840eb
more exports, as in "isabelle dump";

diff -r 75cce7926ec1 -r 27d9aa2a4010 src/Pure/Tools/build_job.scala
--- 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")