changeset 65359 | 9ca34f0407a9 |
parent 65344 | b99283eed13c |
child 65360 | 3ff88fece1f6 |
--- a/src/Pure/Tools/build.scala Mon Apr 03 14:29:44 2017 +0200 +++ b/src/Pure/Tools/build.scala Mon Apr 03 16:36:45 2017 +0200 @@ -220,7 +220,7 @@ ML_Syntax.print_string0(File.platform_path(output)) if (pide && !Sessions.pure_name(name)) { - val resources = new Resources(deps(parent)) + val resources = new Resources(name, deps(parent)) val session = new Session(options, resources) val handler = new Handler(progress, session, name) session.init_protocol_handler(handler)