From 4a62d2324956a21635a6c6a17cd2f16587046be1 Mon Sep 17 00:00:00 2001
From: Benjamin Fischer <benjamin.fischer@rwth-aachen.de>
Date: Thu, 17 Jan 2019 12:38:59 +0100
Subject: [PATCH] [test/bench] kick off polling when we need it during
 execution

---
 test/bench/index.js | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/bench/index.js b/test/bench/index.js
index e52a770f..0201cabd 100644
--- a/test/bench/index.js
+++ b/test/bench/index.js
@@ -84,6 +84,7 @@ class CodeEditor extends View {
 
   async execute(cmd = "python %1") {
     cmd = cmd.replace("%1", JSON.stringify(basename(this.path)));
+    this.user.poll();
     await this.req.post("/extensions/codeeditor/execute", {
       form: { base: dirname(this.path), cmd }
     });
-- 
GitLab