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