git.annexia.org / goals.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec7d2c7) | patch
jobs: Don't let Failure exception escape from worker.
authorRichard W.M. Jones <rjones@redhat.com>
Thu, 9 Jan 2020 11:53:54 +0000 (11:53 +0000)
committerRichard W.M. Jones <rjones@redhat.com>
Thu, 9 Jan 2020 12:14:53 +0000 (12:14 +0000)
commitd06b73832126c575927af40f3ebf574e8621b2a8
treefd89c5e2ea533495132af3aa880050d8efa20ec6tree | snapshot
parentec7d2c76a7ae7447866522103b18107f154083cbcommit | diff
jobs: Don't let Failure exception escape from worker.

Also stop the wait () function if the stop flag is set so we don't
wait forever for jobs which are never going to be run.
src/jobs.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.