# HG changeset patch
# User wenzelm
# Date 1675601847 -3600
# Node ID 198697983eec36bd03ad3695e433f99ba38f1d5c
# Parent  c42bf52381f1358a463c8d368dc0d0f634ac4b4a
more robust dependencies for Pure;

diff -r c42bf52381f1 -r 198697983eec 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)