proper closing order;
authorFabian Huch <huch@in.tum.de>
Thu, 14 Dec 2023 13:03:33 +0100
changeset 79288 92d2473687f0
parent 79287 b88b6ed06334
child 79289 7c1faa16554b
proper closing order;
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()
     }