author | Lars Hupel <lars.hupel@mytum.de> |
Tue, 26 Jun 2018 15:16:22 +0200 | |
changeset 68498 | 6855ebc61b4f |
parent 68497 | f483fe1813f0 |
child 68500 | e3e742b9eed4 |
--- a/src/Pure/Admin/ci_profile.scala Tue Jun 26 10:49:37 2018 +0200 +++ b/src/Pure/Admin/ci_profile.scala Tue Jun 26 15:16:22 2018 +0200 @@ -24,6 +24,7 @@ progress = progress, clean_build = clean, verbose = true, + numa_shuffling = numa, max_jobs = jobs, dirs = include, select_dirs = select, @@ -137,6 +138,7 @@ def documents: Boolean = true def clean: Boolean = true + def numa: Boolean = false def threads: Int def jobs: Int