tuned;
authorwenzelm
Thu, 04 May 2017 12:27:18 +0200
changeset 65714 7693ba6d65bc
parent 65713 b99b48eb46e5
child 65715 e57e5935c6b4
tuned;
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)