# HG changeset patch
# User wenzelm
# Date 1709546736 -3600
# Node ID dbdb8ba05b2b5b8971de51c603891f8b531c8be9
# Parent  5492439ffe89c1cb96c7653f1d8bea8db8707ef1
more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b);

diff -r 5492439ffe89 -r dbdb8ba05b2b src/Pure/Build/build_process.scala
--- 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 _ =>
     }
   }
diff -r 5492439ffe89 -r dbdb8ba05b2b src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun Mar 03 17:47:50 2024 +0100
+++ b/src/Pure/System/progress.scala	Mon Mar 04 11:05:36 2024 +0100
@@ -378,7 +378,7 @@
         (results, true) })
   }
 
-  def exit(close: Boolean = false): Unit = synchronized {
+  def close(): Unit = synchronized {
     if (_context > 0) {
       _consumer.shutdown()
       _consumer = null
@@ -388,7 +388,7 @@
       }
       _context = 0
     }
-    if (close) db.close()
+    db.close()
   }
 
   private def sync_context[A](body: => A): A = synchronized {