# HG changeset patch
# User wenzelm
# Date 1608491645 -3600
# Node ID 2621225b4bdd3a108b46d13a2c04d7d7110656b6
# Parent  f4124c389a621f3a08c1bc807fac8913b9d11d43
proper relative path;

diff -r f4124c389a62 -r 2621225b4bdd src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Dec 20 16:13:30 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Sun Dec 20 20:14:05 2020 +0100
@@ -30,8 +30,7 @@
 
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
       case (Value.Long(id), thy_file :: blobs_files) =>
-        val thy_path = Path.explode(thy_file)
-        val node_name = resources.file_node(thy_path, theory = theory)
+        val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
 
         val results =
           Command.Results.make(
@@ -43,7 +42,7 @@
           {
             val path = Path.explode(file)
             val name = resources.file_node(path)
-            val src_path = File.relative_path(thy_path, path).getOrElse(path)
+            val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
             Command.Blob(name, src_path, None)
           })
         val blobs_xml =