proper detection of ARM platform variants;
authorwenzelm
Fri, 12 Nov 2021 23:20:05 +0100 (2021-11-12)
changeset 74776 251bf0f2d5bb
parent 74774 c60fa7a116b7
child 74777 2fd0c33fe440
proper detection of ARM platform variants;
src/Pure/Admin/build_status.scala
src/Pure/ML/ml_system.ML
--- a/src/Pure/Admin/build_status.scala	Fri Nov 12 18:45:02 2021 +0100
+++ b/src/Pure/Admin/build_status.scala	Fri Nov 12 23:20:05 2021 +0100
@@ -270,9 +270,11 @@
               threads1 max threads2
             }
             val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
+            val ml_platform_64 =
+              ml_platform.startsWith("x86_64-") || ml_platform.startsWith("arm64-")
             val data_name =
               profile.description +
-                (if (ml_platform.startsWith("x86_64-")) ", 64bit" else "") +
+                (if (ml_platform_64) ", 64bit" else "") +
                 (if (threads == 1) "" else ", " + threads + " threads")
 
             res.get_string(Build_Log.Prop.build_host).foreach(host =>
--- a/src/Pure/ML/ml_system.ML	Fri Nov 12 18:45:02 2021 +0100
+++ b/src/Pure/ML/ml_system.ML	Fri Nov 12 23:20:05 2021 +0100
@@ -28,8 +28,8 @@
 val platform_is_macos = String.isSuffix "darwin" platform;
 val platform_is_windows = String.isSuffix "windows" platform;
 val platform_is_unix = platform_is_linux orelse platform_is_macos;
-val platform_is_64 = String.isPrefix "x86_64-" platform;
-val platform_is_arm = String.isPrefix "arm64-" platform;
+val platform_is_64 = String.isPrefix "x86_64-" platform orelse String.isPrefix "arm64-" platform;
+val platform_is_arm = String.isPrefix "arm64_32-" platform orelse String.isPrefix "arm64-" platform;
 
 val platform_path =
   if platform_is_windows then