changeset 73367 | 77ef8bef0593 |
parent 73356 | 819f6033fb4e |
child 73418 | 7d7d959547a1 |
--- a/src/Pure/System/scala.scala Thu Mar 04 19:55:52 2021 +0100 +++ b/src/Pure/System/scala.scala Thu Mar 04 21:04:27 2021 +0100 @@ -114,7 +114,7 @@ if (interpret) interp.interpret(source) == Results.Success else (new interp.ReadEvalPrint).compile(source) } - out.close + out.close() val Error = """(?s)^\S* error: (.*)$""".r val errors = @@ -195,7 +195,7 @@ private def cancel(id: String, future: Future[Unit]): Unit = { - future.cancel + future.cancel() result(id, Scala.Tag.INTERRUPT, "") }