src/Pure/Tools/update.scala
changeset 76928 cd8f6634db17
parent 76927 da13da82f6f9
child 76929 c7a165287df5
equal deleted inserted replaced
76927:da13da82f6f9 76928:cd8f6634db17
    48 
    48 
    49     /* build */
    49     /* build */
    50 
    50 
    51     val build_results =
    51     val build_results =
    52       Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
    52       Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
    53         selection = selection, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
    53         selection = selection, build_heap = build_heap, clean_build = clean_build,
       
    54         numa_shuffling = numa_shuffling, max_jobs = max_jobs,  fresh_build = fresh_build,
    54         no_build = no_build, verbose = verbose, augment_options = augment_options)
    55         no_build = no_build, verbose = verbose, augment_options = augment_options)
    55 
    56 
    56     val store = build_results.store
    57     val store = build_results.store
    57     val sessions_structure = build_results.deps.sessions_structure
    58     val sessions_structure = build_results.deps.sessions_structure
    58 
    59