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 _ => } }