# HG changeset patch # User wenzelm # Date 1493893638 -7200 # Node ID 7693ba6d65bc9ccb2fd1c1201473a041bc7d0fed # Parent b99b48eb46e5490f9dd8bde978ce0bc35e186490 tuned; diff -r b99b48eb46e5 -r 7693ba6d65bc src/Pure/Admin/build_log.scala --- 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)