# HG changeset patch
# User wenzelm
# Date 1676972610 -3600
# Node ID b3f8aad678e95170e969ccbb94740d2da0848887
# Parent  cf6947717650ceed631f318368215f12d073743e
clarified signature;

diff -r cf6947717650 -r b3f8aad678e9 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Feb 21 10:43:30 2023 +0100
@@ -215,7 +215,7 @@
             progress = progress,
             dirs = dirs,
             select_dirs = select_dirs,
-            numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+            numa_shuffling = NUMA.check(progress, numa_shuffling),
             max_jobs = max_jobs,
             verbose = verbose)
         }
diff -r cf6947717650 -r b3f8aad678e9 src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/Pure/System/numa.scala	Tue Feb 21 10:43:30 2023 +0100
@@ -58,7 +58,7 @@
 
   /* shuffling of CPU nodes */
 
-  def enabled_warning(progress: Progress, enabled: Boolean): Boolean = {
+  def check(progress: Progress, enabled: Boolean): Boolean = {
     def warning =
       nodes() match {
         case ns if ns.length < 2 => Some("no NUMA nodes available")
diff -r cf6947717650 -r b3f8aad678e9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/Pure/Tools/build.scala	Tue Feb 21 10:43:30 2023 +0100
@@ -293,7 +293,7 @@
             clean_build = clean_build,
             dirs = dirs,
             select_dirs = select_dirs,
-            numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+            numa_shuffling = NUMA.check(progress, numa_shuffling),
             max_jobs = max_jobs,
             list_files = list_files,
             check_keywords = check_keywords,
diff -r cf6947717650 -r b3f8aad678e9 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/Pure/Tools/update.scala	Tue Feb 21 10:43:30 2023 +0100
@@ -220,7 +220,7 @@
               clean_build,
               dirs = dirs,
               select_dirs = select_dirs,
-              numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+              numa_shuffling = NUMA.check(progress, numa_shuffling),
               max_jobs = max_jobs,
               fresh_build,
               no_build = no_build,