changeset 66963 | 1c3d0c12bb51 |
parent 65477 | 64e61b0f6972 |
child 66964 | 9f2de457b95e |
--- a/src/Pure/ML/ml_console.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Pure/ML/ml_console.scala Tue Oct 31 17:56:28 2017 +0100 @@ -75,7 +75,7 @@ raw_ml_system = raw_ml_system, store = Sessions.store(system_mode), session_base = if (raw_ml_system) None - else Some(Sessions.session_base(options, logic, dirs))) + else Some(Sessions.session_base_info(options, logic, dirs).check)) val process_output = Future.thread[Unit]("process_output") { try { var result = new StringBuilder(100)