src/Pure/Build/build.scala
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