src/Pure/Tools/build_process.scala
changeset 77477 f376aebca9c1
parent 77476 5f6f567a2661
child 77486 032c76e04475
equal deleted inserted replaced
77476:5f6f567a2661 77477:f376aebca9c1
    76                 }
    76                 }
    77               case ord => ord
    77               case ord => ord
    78             }
    78             }
    79         }
    79         }
    80 
    80 
    81       val numa_nodes = NUMA.nodes(enabled = numa_shuffling)
    81       val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
    82       new Context(store, build_deps, sessions, ordering, progress, hostname, numa_nodes,
    82       new Context(store, build_deps, sessions, ordering, progress, hostname, numa_nodes,
    83         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
    83         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
    84         no_build = no_build, verbose = verbose, session_setup, uuid = uuid)
    84         no_build = no_build, verbose = verbose, session_setup, uuid = uuid)
    85     }
    85     }
    86   }
    86   }