support NUMA shuffling in CI
authorLars Hupel <lars.hupel@mytum.de>
Tue, 26 Jun 2018 15:16:22 +0200
changeset 68498 6855ebc61b4f
parent 68497 f483fe1813f0
child 68500 e3e742b9eed4
support NUMA shuffling in CI
src/Pure/Admin/ci_profile.scala
--- 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