equal
deleted
inserted
replaced
73 if (exclude(name)) Nil else update_options |
73 if (exclude(name)) Nil else update_options |
74 |
74 |
75 |
75 |
76 /* build */ |
76 /* build */ |
77 |
77 |
|
78 val build_options = options + "build_thorough" |
|
79 |
78 val build_results = |
80 val build_results = |
79 Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs, |
81 Build.build(build_options, progress = progress, dirs = dirs, select_dirs = select_dirs, |
80 selection = selection, build_heap = build_heap, clean_build = clean_build, |
82 selection = selection, build_heap = build_heap, clean_build = clean_build, |
81 numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, |
83 numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, |
82 no_build = no_build, augment_options = augment_options) |
84 no_build = no_build, augment_options = augment_options) |
83 |
85 |
84 val store = build_results.store |
86 val store = build_results.store |