# HG changeset patch
# User Edouard Tisserant <edouard.tisserant@gmail.com>
# Date 1695987950 -7200
# Node ID c3f4e114af38df3e2314731b1b78cdf4bc994ee1
# Parent  91da73c3df6195c24e559e9a80d47bf517a71980
Fix untested code in worker.py...

diff -r 91da73c3df61 -r c3f4e114af38 runtime/Worker.py
--- 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()