# 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 =>