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))