diff -r 064925cb656f -r 3b197547c1d4 src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Sun May 14 17:19:22 2017 +0200
+++ b/src/Pure/System/numa.scala	Sun May 14 17:19:46 2017 +0200
@@ -42,7 +42,7 @@
 
   /* shuffling of CPU nodes */
 
-  def enabled_warning(enabled: Boolean): Boolean =
+  def enabled_warning(progress: Progress, enabled: Boolean): Boolean =
   {
     def warning =
       if (nodes().length < 2) Some("no NUMA nodes available")
@@ -51,7 +51,7 @@
 
     enabled &&
       (warning match {
-        case Some(s) => Output.warning("Shuffling of CPU nodes is disabled: " + s); false
+        case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false
         case _ => true
       })
   }