# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717436262 -7200
# Node ID 885fc1e837eda0e905997d12e809f42b85d0fe8b
# Parent  b2889dd54a2af59c1bf414722878ae37b4d8fd06
tuned;

diff -r b2889dd54a2a -r 885fc1e837ed src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Mon Jun 03 19:21:22 2024 +0200
+++ b/src/Pure/System/web_app.scala	Mon Jun 03 19:37:42 2024 +0200
@@ -404,19 +404,18 @@
         val head1 =
           if (!auto_reload) head
           else HTML.script("""
-var state = null;
+var state = null
 function heartbeat() {
   fetch(window.location, { method: "HEAD" }).then((http_res) => {
-    const new_state = http_res.headers.get("Content-Digest")
-    if (state === null) state = new_state
-    if (http_res.status === 200 && state !== new_state) {
-      state = new_state
-      window.location.reload()
+    if (http_res.status === 200) {
+      const new_state = http_res.headers.get("Content-Digest")
+      if (state === null) state = new_state
+      else if (state !== new_state) window.location.reload()
     }
-    setTimeout(heartbeat, 1000);
+    setTimeout(heartbeat, 1000)
   })
 }
-setTimeout(heartbeat, 1000);""") :: head
+heartbeat()""") :: head
 
         html(
           XML.elem("head", HTML.head_meta :: head1),