src/Pure/Tools/build_job.scala
changeset 72869 015a61936c13
parent 72868 90e28f005be9
child 72871 17533d0a11b8
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 15:27:41 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 16:35:56 2020 +0100
@@ -36,9 +36,9 @@
         val results =
           Command.Results.make(
             for {
-              tree @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES)
+              elem @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES)
               i <- Markup.Serial.unapply(markup.properties)
-            } yield i -> tree)
+            } yield i -> elem)
 
         val blobs =
           blobs_files.map(file =>