Function stopPing

src/server/web/public/terminal.js:8915–8919

()

      lastPingSent = Date.now();
      sendJSON({ type: "ping" });
    }
  }, PING_INTERVAL_MS);
}
function stopPing() {
  if (pingTimer) clearInterval(pingTimer);
  pingTimer = null;
  latencyEl.textContent = "--";
}