Preserve websocket server IP over reloading the web page.

anlumo · Paul Sokolovsky · commit 03492fef5c68 · 2019-03-02T19:19:38.000+03:00
diff --git a/webrepl.html b/webrepl.html
@@ -97,6 +97,10 @@
 
 (function() {
     window.onload = function() {
+      var url = window.location.hash.substring(1);
+      if (url) {
+        document.getElementById('url').value = 'ws://' + url;
+      }
       var size = calculate_size(self);
       term = new Terminal({
         cols: size[0],
@@ -149,6 +153,7 @@
 }
 
 function connect(url) {
+    window.location.hash = url.substring(5);
     ws = new WebSocket(url);
     ws.binaryType = 'arraybuffer';
     ws.onopen = function() {
