runtime/Worker.py
changeset 3849 c3f4e114af38
parent 3846 cf027bfe2653
child 3851 4e1906d119d5
--- a/runtime/Worker.py	Thu Sep 28 18:39:19 2023 +0200
+++ b/runtime/Worker.py	Fri Sep 29 13:45:50 2023 +0200
@@ -73,7 +73,7 @@
                 self.reraise(_job)
 
         while not self._finish:
-            self.todo.wait_for(self.job is not None)
+            self.todo.wait_for(lambda: self.job is not None)
             self.job.do()
             self.done.notify()