src/Pure/Build/build_job.scala
changeset 81414 ed4ff84e9b21
parent 80872 320bcbf34849
--- a/src/Pure/Build/build_job.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -300,7 +300,7 @@
                 def export_text(name: String, text: String, compress: Boolean = true): Unit =
                   export_(name, List(XML.Text(text)), compress = compress)
 
-                for (command <- snapshot.snippet_command) {
+                for (command <- snapshot.snippet_commands) {
                   export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
                 }