# HG changeset patch
# User wenzelm
# Date 1677753370 -3600
# Node ID a073ac3f3b563a32b6f835c9f33f369ef3de6b56
# Parent  50488bcd99f6c4410aced43f4c1807262160ae46
clarified modules;

diff -r 50488bcd99f6 -r a073ac3f3b56 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 02 11:25:50 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 02 11:36:10 2023 +0100
@@ -1508,6 +1508,11 @@
       (relevant, ok)
     }
 
+    def init_output(name: String): Unit = {
+      clean_output(name)
+      using(open_database(name, output = true))(init_session_info(_, name))
+    }
+
     def check_output(
       name: String,
       sources_shasum: SHA1.Shasum,
diff -r 50488bcd99f6 -r a073ac3f3b56 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Mar 02 11:25:50 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 02 11:36:10 2023 +0100
@@ -596,9 +596,7 @@
     else {
       progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...")
 
-      store.clean_output(session_name)
-      using(store.open_database(session_name, output = true))(
-        store.init_session_info(_, session_name))
+      store.init_output(session_name)
 
       val session_background = build_deps.background(session_name)
       val session_heaps =