tuned;

--- 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 =>