tuned signature;
authorwenzelm
Mon, 06 Mar 2023 10:58:36 +0100
changeset 77535 334a286b2975
parent 77534 fc57886e37dd
child 77536 7c7f1473e51a
tuned signature;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
--- a/src/Pure/Thy/sessions.scala	Mon Mar 06 10:16:40 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 06 10:58:36 2023 +0100
@@ -1410,8 +1410,6 @@
     def output_log(name: String): Path = output_dir + log(name)
     def output_log_gz(name: String): Path = output_dir + log_gz(name)
 
-    def prepare_output_dir(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
-
 
     /* heap */
 
@@ -1477,6 +1475,8 @@
     def open_database(name: String, output: Boolean = false): SQL.Database =
       try_open_database(name, output = output) getOrElse error_database(name)
 
+    def prepare_output(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
+
     def clean_output(name: String): (Boolean, Boolean) = {
       val relevant_db =
         database_server &&
--- a/src/Pure/Tools/build.scala	Mon Mar 06 10:16:40 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Mar 06 10:58:36 2023 +0100
@@ -151,7 +151,7 @@
         build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
         fresh_build = fresh_build, no_build = no_build, session_setup = session_setup)
 
-    store.prepare_output_dir()
+    store.prepare_output()
 
     if (clean_build) {
       for (name <- full_sessions.imports_descendants(full_sessions_selection)) {