equal
deleted
inserted
replaced
373 def parse(engine: String, host: String, start: Date, |
373 def parse(engine: String, host: String, start: Date, |
374 End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]): Meta_Info = |
374 End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]): Meta_Info = |
375 { |
375 { |
376 val build_id = |
376 val build_id = |
377 { |
377 { |
378 val prefix = if (host != "") host else if (engine != "") engine else "" |
378 val prefix = proper_string(host) orElse proper_string(engine) getOrElse "build" |
379 (if (prefix == "") "build" else prefix) + ":" + start.time.ms |
379 prefix + ":" + start.time.ms |
380 } |
380 } |
381 val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine) |
381 val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine) |
382 val build_host = if (host == "") Nil else List(Prop.build_host.name -> host) |
382 val build_host = if (host == "") Nil else List(Prop.build_host.name -> host) |
383 |
383 |
384 val start_date = List(Prop.build_start.name -> print_date(start)) |
384 val start_date = List(Prop.build_start.name -> print_date(start)) |