# HG changeset patch
# User wenzelm
# Date 1687015771 -7200
# Node ID a081ad6c3c4bce4923042dc57e3444f479a2785e
# Parent  cc0bd66eb49858329931eb6bb3fc5a21f60ba2fd
proper close;

diff -r cc0bd66eb498 -r a081ad6c3c4b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Jun 17 15:58:41 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sat Jun 17 17:29:31 2023 +0200
@@ -828,6 +828,7 @@
 
   def close(): Unit = synchronized {
     _database.foreach(_.close())
+    _host_database.foreach(_.close())
     progress match {
       case db_progress: Database_Progress =>
         db_progress.exit()