changeset 72571 | ab4a0b19648a |
parent 72557 | 6345cce0e576 |
child 72613 | d01ea9e3bd2d |
--- a/src/Pure/ML/ml_process.scala Tue Nov 10 12:45:20 2020 +0100 +++ b/src/Pure/ML/ml_process.scala Tue Nov 10 12:48:56 2020 +0100 @@ -32,7 +32,7 @@ val heaps: List[String] = if (raw_ml_system) Nil else { - sessions_structure.selection(Sessions.Selection.session(logic_name)). + sessions_structure.selection(logic_name). build_requirements(List(logic_name)). map(a => File.platform_path(store.the_heap(a))) }