--- a/src/Pure/ML/ml_process.scala Mon Nov 16 23:27:43 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Mon Nov 16 23:49:20 2020 +0100
@@ -201,11 +201,11 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+ val base_info = Sessions.base_info(options, logic, dirs = dirs).check
val store = Sessions.store(options)
-
val result =
- ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
+ ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args,
+ modes = modes, session_base = Some(base_info.base))
.result(
progress_stdout = Output.writeln(_, stdout = true),
progress_stderr = Output.writeln(_))