| changeset 73367 | 77ef8bef0593 |
| parent 73340 | 0ffcad1f6130 |
| child 74141 | bba35ad317ab |
--- a/src/Pure/ML/ml_console.scala Thu Mar 04 19:55:52 2021 +0100 +++ b/src/Pure/ML/ml_console.scala Thu Mar 04 21:04:27 2021 +0100 @@ -74,7 +74,7 @@ else Some(Sessions.base_info( options, logic, dirs = dirs, include_sessions = include_sessions).check.base)) - POSIX_Interrupt.handler { process.interrupt } { + POSIX_Interrupt.handler { process.interrupt() } { new TTY_Loop(process.stdin, process.stdout).join val rc = process.join if (rc != 0) sys.exit(rc)