merged
authorwenzelm
Wed Dec 04 19:55:30 2019 +0100 (2 days ago ago)
changeset 714357b9ff966974f
parent 71433 095cf95d7725
parent 71434 dafa5fce70f1
child 71436 da28fd2852ed
merged
     1.1 --- a/src/Pure/Concurrent/consumer_thread.scala	Wed Dec 04 18:28:24 2019 +0100
     1.2 +++ b/src/Pure/Concurrent/consumer_thread.scala	Wed Dec 04 19:55:30 2019 +0100
     1.3 @@ -104,11 +104,7 @@
     1.4            }
     1.5          }
     1.6  
     1.7 -        if (continue) {
     1.8 -          val msgs1 = msgs.drop(reqs.length)
     1.9 -          val msgs2 = mailbox.receive(timeout = Some(Time.zero))
    1.10 -          main_loop(msgs1 ::: msgs2)
    1.11 -        }
    1.12 +        if (continue) main_loop(msgs.drop(reqs.length))
    1.13          else robust_finish()
    1.14      }
    1.15