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