| changeset 67025 | 961285f581e6 |
| parent 66961 | f855f9aed72f |
| child 67026 | 687c822ee5e3 |
--- a/src/Pure/ML/ml_process.scala Tue Nov 07 15:50:36 2017 +0100 +++ b/src/Pure/ML/ml_process.scala Tue Nov 07 16:44:25 2017 +0100 @@ -32,7 +32,7 @@ if (raw_ml_system) Nil else { val selection = Sessions.Selection(sessions = List(logic_name)) - val (_, selected_sessions) = + val selected_sessions = sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection) selected_sessions.build_requirements(List(logic_name)). map(a => File.platform_path(store.heap(a)))