src/Pure/PIDE/batch_session.scala
changeset 59891 9ce697050455
parent 59720 f893472fff31
child 59892 2a616319c171
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Apr 01 13:32:32 2015 +0200
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Apr 01 15:41:08 2015 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4          dirs = dirs, sessions = List(parent_session)) != 0)
     1.5        new RuntimeException
     1.6  
     1.7 -    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
     1.8 +    val deps = Build.dependencies(verbose = verbose, tree = session_tree)
     1.9      val resources =
    1.10      {
    1.11        val content = deps(parent_session)