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