diff options
Diffstat (limited to 'js/python.js')
| -rw-r--r-- | js/python.js | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/js/python.js b/js/python.js index 9d051fe..d114b7e 100644 --- a/js/python.js +++ b/js/python.js @@ -6,6 +6,7 @@ // a constant var firstCharacterPos = {'line': 0, 'ch': 0}; + //codeq.makePythonTerminalHandler = function (jqConsole, editor, problem_id, activityHandler) { var makePythonTerminalHandler = function (jqConsole, editor, problem_id, activityHandler) { var terminal = codeq.makeConsole(jqConsole, { 'greeting': 'CodeQ Python terminal proxy' @@ -37,7 +38,7 @@ return terminal; }; - var makeActivityHandler = function (editor, problem_id) { + var makeActivityHandler = function (editor, problem_id) { var lastActivityMillis = Date.now(), deltaActivityMillis = function deltaActivityMillisFunc () { var now = Date.now(), |