diff -r 79d14c862560 -r e2e43992f339 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Tue Aug 05 16:04:05 2025 +0200 +++ b/src/Pure/Build/build.scala Tue Aug 05 21:44:54 2025 +0200 @@ -728,16 +728,17 @@ val thy_file = migrate_file(thy_file0) val blobs = - blobs_files0.map { name0 => + blobs_files0.map { case (command_offset, name0) => val name = migrate_file(name0) val file = read_source_file(name0) val bytes = file.bytes val text = decode(bytes.text) val chunk = Symbol.Text_Chunk(text) + val content = Some((file.digest, chunk)) - Command.Blob(Document.Node.Name(name), Path.explode(name), Some((file.digest, chunk))) -> - Document.Blobs.Item(bytes, text, chunk, changed = false) + Command.Blob(command_offset, Document.Node.Name(name), Path.explode(name), content) -> + Document.Blobs.Item(bytes, text, chunk, command_offset = command_offset) } val thy_source = decode(read_source_file(thy_file0).bytes.text)