--- a/src/Pure/Tools/build.scala Tue Jun 27 10:05:33 2023 +0200
+++ b/src/Pure/Tools/build.scala Tue Jun 27 10:24:32 2023 +0200
@@ -172,11 +172,13 @@
build_context.prepare_database()
if (clean_build) {
- for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
- store.clean_output(name) match {
- case None =>
- case Some(true) => progress.echo("Cleaned " + name)
- case Some(false) => progress.echo(name + " FAILED to clean")
+ using_optional(store.maybe_open_database_server()) { database_server =>
+ for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
+ store.clean_output(database_server, name) match {
+ case None =>
+ case Some(true) => progress.echo("Cleaned " + name)
+ case Some(false) => progress.echo(name + " FAILED to clean")
+ }
}
}
}