src/Pure/Admin/build_status.scala
changeset 69734 e58f158c8ac5
parent 69693 06153e2e0cdb
child 69740 18d383f41477
equal deleted inserted replaced
69733:6d158fd15b85 69734:e58f158c8ac5
   258               threads1 max threads2
   258               threads1 max threads2
   259             }
   259             }
   260             val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
   260             val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
   261             val data_name =
   261             val data_name =
   262               profile.description +
   262               profile.description +
   263                 (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") +
   263                 (if (ml_platform.startsWith("x86_64-")) ", 64bit" else "") +
   264                 (if (threads == 1) "" else ", " + threads + " threads")
   264                 (if (threads == 1) "" else ", " + threads + " threads")
   265 
   265 
   266             res.get_string(Build_Log.Prop.build_host).foreach(host =>
   266             res.get_string(Build_Log.Prop.build_host).foreach(host =>
   267               data_hosts += (data_name -> (get_hosts(data_name) + host)))
   267               data_hosts += (data_name -> (get_hosts(data_name) + host)))
   268 
   268