changeset 82147 | 3f7c8e6d3481 |
parent 81414 | ed4ff84e9b21 |
--- a/src/Pure/Build/build.scala Wed Feb 12 14:26:43 2025 +0100 +++ b/src/Pure/Build/build.scala Wed Feb 12 14:28:32 2025 +0100 @@ -728,7 +728,7 @@ val blobs = blobs_files.map { name => val path = Path.explode(name) - val src_path = File.relative_path(master_dir, path).getOrElse(path) + val src_path = File.perhaps_relative_path(master_dir, path) val file = read_source_file(name) val bytes = file.bytes