# HG changeset patch
# User wenzelm
# Date 1713279255 -7200
# Node ID 455ddb251ece5cbb780a063238025029d70b01a1
# Parent  7e4c3bb3d0626f6ea246c559268c7ea1a5127f48
clarified signature;

diff -r 7e4c3bb3d062 -r 455ddb251ece src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/Build/build_benchmark.scala	Tue Apr 16 16:54:15 2024 +0200
@@ -66,12 +66,7 @@
         for (db <- database_server) ML_Heap.restore(db, hierachy, cache = store.cache.compress)
 
         def get_shasum(session_name: String): SHA1.Shasum = {
-          val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
-
-          val input_shasum =
-            if (ancestor_shasums.isEmpty) ML_Process.bootstrap_shasum()
-            else SHA1.flat_shasum(ancestor_shasums)
-
+          val input_shasum = ML_Process.make_shasum(sessions(session_name).ancestors.map(get_shasum))
           store.check_output(
             database_server, session_name,
             session_options = build_context.sessions_structure(session_name).options,
diff -r 7e4c3bb3d062 -r 455ddb251ece src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/Build/build_process.scala	Tue Apr 16 16:54:15 2024 +0200
@@ -1163,13 +1163,8 @@
     ancestor_results: List[Build_Process.Result]
   ): Build_Process.State = {
     val sources_shasum = state.sessions(session_name).sources_shasum
-
-    val input_shasum =
-      if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
-      else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
-
+    val input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum))
     val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
-
     val (current, output_shasum) =
       store.check_output(_database_server, session_name,
         session_options = build_context.sessions_structure(session_name).options,
diff -r 7e4c3bb3d062 -r 455ddb251ece src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala	Tue Apr 16 16:54:15 2024 +0200
@@ -1120,9 +1120,7 @@
         case Some(ancestor_results) if ancestor_results.forall(_.current) =>
           val sources_shasum = state.sessions(session_name).sources_shasum
 
-          val input_shasum =
-            if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
-            else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
+          val input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum))
 
           val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
 
diff -r 7e4c3bb3d062 -r 455ddb251ece src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/ML/ml_process.scala	Tue Apr 16 16:54:15 2024 +0200
@@ -12,8 +12,9 @@
 
 
 object ML_Process {
-  def bootstrap_shasum(): SHA1.Shasum =
-    SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+  def make_shasum(ancestors: List[SHA1.Shasum]): SHA1.Shasum =
+    if (ancestors.isEmpty) SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+    else SHA1.flat_shasum(ancestors)
 
   def session_heaps(
     store: Store,