| <!DOCTYPE html> |
| <html> |
| <head> |
| <title>Launch Time Benchmark</title> |
| <script src="http://code.jquery.com/jquery-1.9.1.min.js"></script> |
| </head> |
| <body style="font-family: -apple-system; font-size:1.5em;"> |
| <h2>Benchmark Progress</h2> |
| <p id="output" style="white-space: pre-line;"></p> |
| <strong id="done"></strong> |
| </body> |
| </html> |
| <script> |
| if (!("WebSocket" in window)) { |
| alert("Your browser does not support web sockets"); |
| } else { |
| setup(); |
| } |
| |
| function setup() { |
| const host = "ws://localhost:{{ port }}/ws"; |
| const socket = new WebSocket(host); |
| |
| if (socket) { |
| socket.onmessage = message => showServerMessage(message.data); |
| socket.onclose = () => document.getElementById('done').textContent = 'DONE'; |
| } else { |
| console.log("invalid socket"); |
| } |
| |
| function showServerMessage(text) { |
| text = text.replace(/\n/g, "\r\n"); |
| const output = document.getElementById('output'); |
| output.textContent = output.textContent.concat(text) |
| } |
| } |
| </script> |
