# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1724759598 -7200
# Node ID 32247ad40647fb10c1442c817f614c59f5d07169
# Parent  11e33f3d5ef1f0fd40d05ea370e1802296e22d8e
stop web server on close;

diff -r 11e33f3d5ef1 -r 32247ad40647 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() }
   }