src/Pure/Tools/build.scala
changeset 65315 c7097ccbffb7
parent 65314 944758d6462e
child 65317 b9f5cd845616
     1.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 20:57:15 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 21:24:54 2017 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4            val resources = new Resources(deps(parent))
     1.5            val session = new Session(options, resources)
     1.6            val handler = new Handler(progress, session, name)
     1.7 -          session.add_protocol_handler(handler)
     1.8 +          session.init_protocol_handler(handler)
     1.9  
    1.10            val session_result = Future.promise[Int]
    1.11