src/Pure/Build/store.scala
changeset 79709 90fbcdafb34e
parent 79708 f25a6b4c3e41
child 79711 5044f1d9196d
--- 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(