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