changeset 72871 | 17533d0a11b8 |
parent 72869 | 015a61936c13 |
child 72873 | 0ad513706a27 |
--- 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 =>