changeset 67803 | 1cf4126d7bd9 |
parent 67802 | 32d76f08023f |
child 67808 | 9cb7f5f0bf41 |
--- a/src/Pure/ML/ml_console.scala Fri Mar 09 17:03:10 2018 +0100 +++ b/src/Pure/ML/ml_console.scala Sat Mar 10 11:08:20 2018 +0100 @@ -77,7 +77,7 @@ val tty_loop = new TTY_Loop(process.stdin, process.stdout, process.interrupt _) val process_result = Future.thread[Int]("process_result") { val rc = process.join - tty_loop.cancel + tty_loop.cancel // FIXME does not quite work, cannot interrupt blocking read on System.in rc } tty_loop.join