# HG changeset patch
# User wenzelm
# Date 1688317012 -7200
# Node ID 633ae08625d1534463d29ec8ec99d0525627c5ab
# Parent  39e1562e69cdc4b6889567108a8fdd089973e214
clarified signature;

diff -r 39e1562e69cd -r 633ae08625d1 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun Jul 02 15:39:51 2023 +0200
+++ b/src/Pure/System/progress.scala	Sun Jul 02 18:56:52 2023 +0200
@@ -287,13 +287,14 @@
     if (context_uuid == _agent_uuid) Progress.Data.vacuum(db)
   }
 
-  def exit(): Unit = synchronized {
+  def exit(close: Boolean = false): Unit = synchronized {
     if (_context > 0) {
       Progress.Data.transaction_lock(db) {
         Progress.Data.update_agent(db, _agent_uuid, _seen, stop = true)
       }
       _context = 0
     }
+    if (close) db.close()
   }
 
   private def sync_database[A](body: => A): A = synchronized {
diff -r 39e1562e69cd -r 633ae08625d1 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Jul 02 15:39:51 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 02 18:56:52 2023 +0200
@@ -883,8 +883,7 @@
     Option(_host_database).flatten.foreach(_.close())
     progress match {
       case db_progress: Database_Progress =>
-        db_progress.exit()
-        db_progress.db.close()
+        db_progress.exit(close = true)
       case _ =>
     }
   }