author | wenzelm |
Wed, 01 Apr 2020 12:59:05 +0200 | |
changeset 71643 | 43ba9fece20d |
parent 71642 | 77327455b00d |
child 71644 | 60659474ed36 |
--- a/src/Pure/Tools/build.scala Wed Apr 01 12:58:44 2020 +0200 +++ b/src/Pure/Tools/build.scala Wed Apr 01 12:59:05 2020 +0200 @@ -252,8 +252,8 @@ } else Nil - if (pide && !is_pure) { - val resources = new Resources(sessions_structure, deps(name)) + if (pide) { + val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) val handler = new Handler(progress, session, name) session.init_protocol_handler(handler)