# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1530018982 -7200
# Node ID 6855ebc61b4f38e2baf3b22fa731406e70dc0f53
# Parent  f483fe1813f0c5959eb6311af8dd39f1c6af9ed7
support NUMA shuffling in CI

diff -r f483fe1813f0 -r 6855ebc61b4f 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