# HG changeset patch
# User wenzelm
# Date 1672485382 -3600
# Node ID ef1f7d56f7c8acfd2ee2035053f84d6fbb5badcf
# Parent  3dfc89c8dd7109913b4e1177b1ffa2e6e070c6e1
tuned: no need to map master_dir, which does not participate in comparison;

diff -r 3dfc89c8dd71 -r ef1f7d56f7c8 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Dec 31 12:10:14 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Dec 31 12:16:22 2022 +0100
@@ -274,8 +274,8 @@
           override val cache: Term.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
-            val name1 = name.map(s => Path.explode(s).expand.implode)
-            session_background.base.load_commands.get(name1) match {
+            val expand_node = Document.Node.Name(Path.explode(name.node).expand.implode)
+            session_background.base.load_commands.get(expand_node) match {
               case Some(spans) =>
                 val syntax = session_background.base.theory_syntax(name)
                 Command.build_blobs_info(syntax, name, spans)