From af14c7d8871c2525d362dc300aa73ba3e8bcca6e Mon Sep 17 00:00:00 2001 From: annasandri Date: Thu, 28 May 2020 11:30:04 +0200 Subject: [PATCH] Update '12/pipeserver.js' --- 12/pipeserver.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/12/pipeserver.js b/12/pipeserver.js index d7bd5a4..fa7d5a8 100644 --- a/12/pipeserver.js +++ b/12/pipeserver.js @@ -1,6 +1,6 @@ var ws_addr = 'wss://'+window.location.host+"/12/pipe", sock = null, - //shell = document.getElementById("shell"), + shell = document.getElementById("shell"), authors = document.getElementById("authors"), title = document.getElementById("title"), connections = document.getElementById("connections");