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