# HG changeset patch
# User wenzelm
# Date 1687338904 -7200
# Node ID 26b9b40ec1afbcff278b417d08eae94ed694ad3f
# Parent  4309bcc8f28b260b8279a2a878ca2ebf42f988c7
tuned signature;

diff -r 4309bcc8f28b -r 26b9b40ec1af src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Wed Jun 21 11:05:20 2023 +0200
+++ b/src/Pure/Thy/store.scala	Wed Jun 21 11:15:04 2023 +0200
@@ -299,7 +299,7 @@
 
   def prepare_output(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
 
-  def clean_output(name: String): Option[Boolean] = {
+  def clean_output(name: String, init: Boolean = false): Option[Boolean] = {
     val relevant_db =
       build_database_server &&
         using_option(try_open_database(name))(init_session_info(_, name)).getOrElse(false)
@@ -312,12 +312,9 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
-    if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
-  }
+    if (init) using(open_database(name, output = true))(init_session_info(_, name))
 
-  def init_output(name: String): Unit = {
-    clean_output(name)
-    using(open_database(name, output = true))(init_session_info(_, name))
+    if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
   }
 
   def check_output(
diff -r 4309bcc8f28b -r 26b9b40ec1af src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Jun 21 11:05:20 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jun 21 11:15:04 2023 +0200
@@ -939,7 +939,7 @@
         (if (store_heap) "Building " else "Running ") + session_name +
           if_proper(node_info.numa_node, " on " + node_info) + " ...")
 
-      store.init_output(session_name)
+      store.clean_output(session_name, init = true)
 
       val build =
         Build_Job.start_session(build_context, progress, log,