equal
deleted
inserted
replaced
214 List("ML_Heap.save_child " + |
214 List("ML_Heap.save_child " + |
215 ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) |
215 ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) |
216 } |
216 } |
217 else Nil |
217 else Nil |
218 |
218 |
219 if (options.bool("pide_session")) { |
219 if (options.bool("pide_session") || true /* FIXME test */) { |
220 val resources = new Resources(sessions_structure, deps(parent)) |
220 val resources = new Resources(sessions_structure, deps(parent)) |
221 val session = |
221 val session = |
222 new Session(options, resources) { |
222 new Session(options, resources) { |
223 override val xml_cache: XML.Cache = store.xml_cache |
223 override val xml_cache: XML.Cache = store.xml_cache |
224 override val xz_cache: XZ.Cache = store.xz_cache |
224 override val xz_cache: XZ.Cache = store.xz_cache |