src/Pure/Tools/build_job.scala
changeset 76930 9ce0aa145d21
parent 76913 a8eb5046b05f
child 76933 dd53bb198eb1
--- a/src/Pure/Tools/build_job.scala	Fri Jan 06 14:37:55 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Jan 06 14:58:13 2023 +0100
@@ -427,7 +427,8 @@
               cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))),
               compress = false)
 
-            for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
+            for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) {
+              val xml = snapshot.switch(blob_name).xml_markup()
               export_(Export.MARKUP + (i + 1), xml)
             }
             export_(Export.MARKUP, snapshot.xml_markup())