Commit 4a62d232 authored by Benjamin Fischer's avatar Benjamin Fischer

[test/bench] kick off polling when we need it during execution

parent 705349cf
...@@ -84,6 +84,7 @@ class CodeEditor extends View { ...@@ -84,6 +84,7 @@ class CodeEditor extends View {
async execute(cmd = "python %1") { async execute(cmd = "python %1") {
cmd = cmd.replace("%1", JSON.stringify(basename(this.path))); cmd = cmd.replace("%1", JSON.stringify(basename(this.path)));
this.user.poll();
await this.req.post("/extensions/codeeditor/execute", { await this.req.post("/extensions/codeeditor/execute", {
form: { base: dirname(this.path), cmd } form: { base: dirname(this.path), cmd }
}); });
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment