author | wenzelm |
Wed, 04 Dec 2019 19:55:30 +0100 | |
changeset 71232 | 7b9ff966974f |
parent 71230 | 095cf95d7725 (current diff) |
parent 71231 | dafa5fce70f1 (diff) |
child 71233 | da28fd2852ed |
--- a/src/Pure/Concurrent/consumer_thread.scala Wed Dec 04 18:28:24 2019 +0100 +++ b/src/Pure/Concurrent/consumer_thread.scala Wed Dec 04 19:55:30 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() }