--- a/src/Pure/Build/build.scala Thu Feb 22 20:54:51 2024 +0100
+++ b/src/Pure/Build/build.scala Thu Feb 22 21:03:55 2024 +0100
@@ -252,11 +252,7 @@
if (clean_build) {
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")
- }
+ store.clean_output(database_server, name, progress = progress)
}
}
--- a/src/Pure/Build/store.scala Thu Feb 22 20:54:51 2024 +0100
+++ b/src/Pure/Build/store.scala Thu Feb 22 21:03:55 2024 +0100
@@ -431,8 +431,9 @@
def clean_output(
database_server: Option[SQL.Database],
name: String,
- session_init: Boolean = false
- ): Option[Boolean] = {
+ session_init: Boolean = false,
+ progress: Progress = new Progress
+ ): Unit = {
val relevant_db =
database_server match {
case Some(db) => clean_session_info(db, name)
@@ -450,7 +451,10 @@
using(open_database(name, output = true))(clean_session_info(_, name))
}
- if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
+ if (relevant_db || del.nonEmpty) {
+ if (del.forall(identity)) progress.echo("Cleaned " + name)
+ else progress.echo(name + " FAILED to clean")
+ }
}
def check_output(