src/Pure/System/web_app.scala
changeset 80243 b2889dd54a2a
parent 80206 3cf3ad092e3e
child 80244 885fc1e837ed
--- a/src/Pure/System/web_app.scala	Mon Jun 03 20:56:41 2024 +0100
+++ b/src/Pure/System/web_app.scala	Mon Jun 03 19:21:22 2024 +0200
@@ -407,7 +407,7 @@
 var state = null;
 function heartbeat() {
   fetch(window.location, { method: "HEAD" }).then((http_res) => {
-    const new_state = http_res.headers.get("Content-Length")
+    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