diff --git a/docs.it4i/js/tty-player.js b/docs.it4i/js/tty-player.js index d84f06367e66e76fffabf50bdfad9030d8dd8f4d..90853f58e8ed01139d090b74d5d338a83753b2d7 100644 --- a/docs.it4i/js/tty-player.js +++ b/docs.it4i/js/tty-player.js @@ -423,9 +423,9 @@ ISP.setUp = function() { ttyPlayer.appendChild(self.titleElement); self.terminal = new Terminal({"useFocus": false}); - self.terminal.on("title", function(newTitle) { + /*self.terminal.on("title", function(newTitle) { ttyPlayer["title"] = newTitle; - }); + });*/ self.terminal.open(ttyPlayer);