# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710805329 -3600
# Node ID 08b83f91a1b2e5b73dc0889a88e60c876595c956
# Parent  cdc87eed26c75a00aa9819d40fa964c14fa7edb6
disable taskset for now: performance impact is negative;

diff -r cdc87eed26c7 -r 08b83f91a1b2 src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Sun Mar 17 22:48:44 2024 +0100
+++ b/src/Pure/System/host.scala	Tue Mar 19 00:42:09 2024 +0100
@@ -77,8 +77,9 @@
         threads_options.string.update("process_policy",
           if (numactl_ok(numa_node, node.rel_cpus)) numactl(numa_node, node.rel_cpus) else "")
       case _ =>
-        threads_options.string.update("process_policy",
-          if (taskset_ok(node.rel_cpus)) taskset(node.rel_cpus) else "")
+        // FIXME threads_options.string.update("process_policy",
+        //  if (taskset_ok(node.rel_cpus)) taskset(node.rel_cpus) else "")
+        threads_options
     }
   }