src/Pure/Concurrent/consumer_thread.scala
changeset 78592 fdfe9b91d96e
parent 78534 879e1ba3868b
child 78864 2024a2298d7a
--- a/src/Pure/Concurrent/consumer_thread.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -89,7 +89,7 @@
 
     val (results, cont) = consume(reqs.map(_.arg))
     for {
-      (Some(req), Some(res)) <- reqs.map(Some(_)).zipAll(results.map(Some(_)), None, None)
+      case (Some(req), Some(res)) <- reqs.map(Some(_)).zipAll(results.map(Some(_)), None, None)
     } {
       (req.ack, res) match {
         case (Some(a), _) => a.change(_ => Some(res))