--- 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
})
}