src/Pure/Build/build_process.scala
changeset 79760 dbdb8ba05b2b
parent 79717 da4e82434985
child 79762 de611b17762c
--- a/src/Pure/Build/build_process.scala	Sun Mar 03 17:47:50 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Mon Mar 04 11:05:36 2024 +0100
@@ -935,7 +935,7 @@
     Option(_host_database).foreach(_.close())
     Option(_build_cluster).foreach(_.close())
     progress match {
-      case db_progress: Database_Progress => db_progress.exit(close = true)
+      case db_progress: Database_Progress => db_progress.close()
       case _ =>
     }
   }