# HG changeset patch # User paulson # Date 1548341107 0 # Node ID 25d539a4b5bbb595d429f3666b6208e614fec32f # Parent e58f158c8ac5a3f616790f9e6a735adc030fe815# Parent 8230dca028ebf844b5e9fc0483a18d7f40935c77 merged diff -r 8230dca028eb -r 25d539a4b5bb src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Thu Jan 24 14:44:52 2019 +0000 +++ b/src/Pure/Admin/build_status.scala Thu Jan 24 14:45:07 2019 +0000 @@ -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 =>