src/Pure/Tools/build.scala
changeset 72076 bd9d1ce274c9
parent 72022 45865bb06182
child 72103 7b318273a4aa
equal deleted inserted replaced
72075:9c0b835d4cc2 72076:bd9d1ce274c9
   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