more robust dependencies for Pure;
authorwenzelm
Sun, 05 Feb 2023 13:57:27 +0100
changeset 77192 198697983eec
parent 77191 c42bf52381f1
child 77193 014c3d00e0f1
more robust dependencies for Pure;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Feb 05 13:13:59 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sun Feb 05 13:57:27 2023 +0100
@@ -380,7 +380,11 @@
                 val ancestor_results =
                   build_deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
-                val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
+                val ancestor_heaps =
+                  if (ancestor_results.isEmpty) {
+                    List(SHA1.digest(Path.explode("$POLYML_EXE")).toString)
+                  }
+                  else ancestor_results.flatMap(_.heap_digest)
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)