more robust result of migrate_file: retain full src_path (in contrast to d5d0e36eda16);
authorwenzelm
Mon, 30 Jun 2025 11:28:04 +0200
changeset 82797 09904d5ef1f0
parent 82796 ad3860303ebb
child 82798 16e2ce15df90
more robust result of migrate_file: retain full src_path (in contrast to d5d0e36eda16);
src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sun Jun 29 16:16:22 2025 +0200
+++ b/src/Pure/Build/build.scala	Mon Jun 30 11:28:04 2025 +0200
@@ -734,15 +734,13 @@
       val blobs =
         blobs_files0.map { name0 =>
           val name = migrate_file(name0)
-          val path = Path.explode(name)
-          val src_path = File.perhaps_relative_path(master_dir, path)
 
           val file = read_source_file(name0)
           val bytes = file.bytes
           val text = decode(bytes.text)
           val chunk = Symbol.Text_Chunk(text)
 
-          Command.Blob(Document.Node.Name(name), src_path, 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)
         }