stop web server on close;
authorFabian Huch <huch@in.tum.de>
Tue, 27 Aug 2024 13:53:18 +0200
changeset 80782 32247ad40647
parent 80781 11e33f3d5ef1
child 80783 14ed085de388
stop web server on close;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Aug 27 13:44:23 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Aug 27 13:53:18 2024 +0200
@@ -1515,11 +1515,14 @@
 html { background-color: white; }"""))
     }
 
+    override def close(): Unit = {
+      server.stop()
+      super.close()
+    }
+
     def init: Unit = server.start()
-    def loop_body(u: Unit): Unit = {
-      if (progress.stopped) server.stop()
-      else synchronized_database("iterate") { cache.update() }
-    }
+    def loop_body(u: Unit): Unit =
+      if (!progress.stopped) synchronized_database("iterate") { cache.update() }
   }