author | wenzelm |
Wed, 27 Jan 2016 14:09:58 +0100 | |
changeset 62247 | ec35b8aca636 |
parent 62246 | d9410066dbd5 |
child 62248 | dca0bac351b2 |
--- a/src/Pure/Concurrent/future.scala Mon Jan 25 14:51:04 2016 +0100 +++ b/src/Pure/Concurrent/future.scala Wed Jan 27 14:09:58 2016 +0100 @@ -88,7 +88,7 @@ status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result)) } } - private val task = Standard_Thread.pool.submit(new Callable[A] { def call = body }) + private val task = Standard_Thread.pool.submit(new Callable[Unit] { def call = try_run() }) def join_result: Exn.Result[A] = {