--- a/src/Pure/ML/ml_console.scala Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Pure/ML/ml_console.scala Tue Oct 31 18:45:33 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_info(options, logic, dirs).check))
+ else Some(Sessions.session_base_info(options, logic, dirs).check_base))
val process_output = Future.thread[Unit]("process_output") {
try {
var result = new StringBuilder(100)