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