# HG changeset patch
# User wenzelm
# Date 1678786541 -3600
# Node ID b1ca8975490acf39ae2f4cd1d38aeecf7930c834
# Parent  739cb777cc758d2e1a8adc627c805332c62911c9
clarified modules;

diff -r 739cb777cc75 -r b1ca8975490a src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Mar 14 10:27:17 2023 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Mar 14 10:35:41 2023 +0100
@@ -12,6 +12,9 @@
 
 
 object ML_Process {
+  def bootstrap_shasum(): SHA1.Shasum =
+    SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+
   def session_heaps(
     store: Sessions.Store,
     session_background: Sessions.Background,
diff -r 739cb777cc75 -r b1ca8975490a src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 10:27:17 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 10:35:41 2023 +0100
@@ -937,9 +937,7 @@
       for (a <- build_context.sessions(session_name).ancestors) yield state.results(a)
 
     val input_shasum =
-      if (ancestor_results.isEmpty) {
-        SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
-      }
+      if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
       else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
 
     val store_heap = build_context.store_heap(session_name)