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) }