diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/tty_loop.scala --- a/src/Pure/System/tty_loop.scala Thu Mar 04 19:55:52 2021 +0100 +++ b/src/Pure/System/tty_loop.scala Thu Mar 04 21:04:27 2021 +0100 @@ -30,7 +30,7 @@ if (result.nonEmpty) { System.out.print(result.toString) System.out.flush() - result.clear + result.clear() } else { reader.close() @@ -64,5 +64,5 @@ def join: Unit = { console_output.join; console_input.join } - def cancel: Unit = console_input.cancel + def cancel(): Unit = console_input.cancel() }