Update '12/pipeserver.js'

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");