# HG changeset patch
# User wenzelm
# Date 1536439932 -7200
# Node ID 122c0d6cb7904e9ea27fafca80d4ad3293ddb2da
# Parent  0851db8cde124c99d3d3b2de5c5073b165c26d06
tuned message;

diff -r 0851db8cde12 -r 122c0d6cb790 src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Sat Sep 08 22:43:25 2018 +0200
+++ b/src/Pure/System/numa.scala	Sat Sep 08 22:52:12 2018 +0200
@@ -56,7 +56,7 @@
   {
     def warning =
       if (nodes().length < 2) Some("no NUMA nodes available")
-      else if (!numactl_available) Some("missing numactl tool")
+      else if (!numactl_available) Some("bad numactl tool")
       else None
 
     enabled &&