changeset 71231 | dafa5fce70f1 |
parent 71144 | d6b9dead8c8d |
child 71685 | d5773922358d |
--- a/src/Pure/Concurrent/consumer_thread.scala Wed Dec 04 15:36:58 2019 +0100 +++ b/src/Pure/Concurrent/consumer_thread.scala Wed Dec 04 19:40:22 2019 +0100 @@ -104,11 +104,7 @@ } } - if (continue) { - val msgs1 = msgs.drop(reqs.length) - val msgs2 = mailbox.receive(timeout = Some(Time.zero)) - main_loop(msgs1 ::: msgs2) - } + if (continue) main_loop(msgs.drop(reqs.length)) else robust_finish() }