215
215
* to its response by writing to the output box.
216
216
* Also maximize the console window if not already.
220
222
var args = {"key": server_key, "text":inputline};
221
225
var callback = function(xhr)
223
227
console_response(inputline, xhr.responseText);
225
235
ajax_call(callback, "consoleservice", which, args, "POST");