changeset 75920 | 27bf2533f4a4 |
parent 75393 | 87ebf5a50283 |
child 76655 | b3d458a90aeb |
--- a/src/Pure/ML/ml_console.scala Sat Aug 20 13:16:15 2022 +0200 +++ b/src/Pure/ML/ml_console.scala Sat Aug 20 13:28:31 2022 +0200 @@ -70,7 +70,7 @@ session_base = if (raw_ml_system) None else Some(Sessions.base_info( - options, logic, dirs = dirs, include_sessions = include_sessions).check.base)) + options, logic, dirs = dirs, include_sessions = include_sessions).check_errors.base)) POSIX_Interrupt.handler { process.interrupt() } { new TTY_Loop(process.stdin, process.stdout).join()