changeset 74141 | bba35ad317ab |
parent 73367 | 77ef8bef0593 |
child 74306 | a117c076aa22 |
--- a/src/Pure/ML/ml_console.scala Sat Aug 07 19:58:38 2021 +0200 +++ b/src/Pure/ML/ml_console.scala Sat Aug 07 21:25:47 2021 +0200 @@ -75,8 +75,8 @@ options, logic, dirs = dirs, include_sessions = include_sessions).check.base)) POSIX_Interrupt.handler { process.interrupt() } { - new TTY_Loop(process.stdin, process.stdout).join - val rc = process.join + new TTY_Loop(process.stdin, process.stdout).join() + val rc = process.join() if (rc != 0) sys.exit(rc) } }