--- 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,
--- 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 =