src/Pure/Tools/build.scala
changeset 66848 982baed14542
parent 66841 5c32a072ca8b
child 66873 9953ae603a23
     1.1 --- a/src/Pure/Tools/build.scala	Thu Oct 12 05:37:58 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Oct 12 11:25:06 2017 +0200
     1.3 @@ -560,7 +560,9 @@
     1.4              //{{{ check/start next job
     1.5              pending.dequeue(running.isDefinedAt(_)) match {
     1.6                case Some((name, info)) =>
     1.7 -                val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
     1.8 +                val ancestor_results =
     1.9 +                  selected_sessions.build_requirements(List(name)).filterNot(_ == name).
    1.10 +                    map(results(_))
    1.11                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    1.12  
    1.13                  val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)