# HG changeset patch
# User wenzelm
# Date 1708632235 -3600
# Node ID 90fbcdafb34ec703ee53953a736564a026a66bfa
# Parent  f25a6b4c3e41dc83b8186d124b341de03bc380d5
clarified signature;

diff -r f25a6b4c3e41 -r 90fbcdafb34e src/Pure/Build/build.scala
--- 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)
           }
         }
 
diff -r f25a6b4c3e41 -r 90fbcdafb34e src/Pure/Build/store.scala
--- 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(