# HG changeset patch
# User wenzelm
# Date 1607616074 -3600
# Node ID 17533d0a11b8c8344344a941a5af9b3b0e28386f
# Parent  8c468d602db196ebf983dbafe6d46c5f29007411
tuned;

diff -r 8c468d602db1 -r 17533d0a11b8 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 16:47:06 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 17:01:14 2020 +0100
@@ -35,10 +35,8 @@
 
         val results =
           Command.Results.make(
-            for {
-              elem @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES)
-              i <- Markup.Serial.unapply(markup.properties)
-            } yield i -> elem)
+            for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
+              yield i -> elem)
 
         val blobs =
           blobs_files.map(file =>