--- a/src/Pure/Admin/build_log.scala Thu May 04 12:23:14 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Thu May 04 12:27:18 2017 +0200
@@ -375,8 +375,8 @@
{
val build_id =
{
- val prefix = if (host != "") host else if (engine != "") engine else ""
- (if (prefix == "") "build" else prefix) + ":" + start.time.ms
+ val prefix = proper_string(host) orElse proper_string(engine) getOrElse "build"
+ prefix + ":" + start.time.ms
}
val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine)
val build_host = if (host == "") Nil else List(Prop.build_host.name -> host)