src/Pure/ML/ml_console.scala
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)
       }
     }