# HG changeset patch
# User wenzelm
# Date 1575485730 -3600
# Node ID 7b9ff966974f9657a39a682cd7eb0f39c159d2b5
# Parent  095cf95d77255120efca21fa3ec3cb3799f51aae# Parent  dafa5fce70f1931aac3dac40dfff19a1b689fa9e
merged

diff -r 095cf95d7725 -r 7b9ff966974f src/Pure/Concurrent/consumer_thread.scala
--- 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()
     }