# HG changeset patch
# User wenzelm
# Date 1548334413 -3600
# Node ID e58f158c8ac5a3f616790f9e6a735adc030fe815
# Parent  6d158fd15b85602d316b2a9a8934718c9bd46801
proper treatment of x86_64_32;

diff -r 6d158fd15b85 -r e58f158c8ac5 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Thu Jan 24 10:04:32 2019 +0100
+++ b/src/Pure/Admin/build_status.scala	Thu Jan 24 13:53:33 2019 +0100
@@ -260,7 +260,7 @@
             val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
             val data_name =
               profile.description +
-                (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") +
+                (if (ml_platform.startsWith("x86_64-")) ", 64bit" else "") +
                 (if (threads == 1) "" else ", " + threads + " threads")
 
             res.get_string(Build_Log.Prop.build_host).foreach(host =>