diff -r 5cb9fd414e92 -r b2889dd54a2a src/Pure/System/web_app.scala --- 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