# HG changeset patch # User wenzelm # Date 1678096716 -3600 # Node ID 334a286b297539e3636fd1c3754df03d40073b4e # Parent fc57886e37dd6112849df9e4b524acc175b35ecd tuned signature; diff -r fc57886e37dd -r 334a286b2975 src/Pure/Thy/sessions.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 && diff -r fc57886e37dd -r 334a286b2975 src/Pure/Tools/build.scala --- 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)) {