# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1702555413 -3600
# Node ID 92d2473687f0108f483961e0e991532d40e8448e
# Parent  b88b6ed0633456a346f4537f1e8b2380fa12accd
proper closing order;

diff -r b88b6ed06334 -r 92d2473687f0 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Wed Dec 13 11:14:11 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Dec 14 13:03:33 2023 +0100
@@ -838,9 +838,9 @@
       catch { case exn: Throwable => close(); throw exn }
 
     override def close(): Unit = {
-      super.close()
       Option(_log_database).foreach(_.close())
       Option(_build_database).flatten.foreach(_.close())
+      super.close()
     }