clarified: use progress start date;
authorFabian Huch <huch@in.tum.de>
Fri, 28 Jun 2024 10:58:29 +0200
changeset 80417 10ab5a74f6f5
parent 80416 c369b0419172
child 80418 9f90c4864e55
clarified: use progress start date;
src/Pure/Build/build_ci.scala
--- a/src/Pure/Build/build_ci.scala	Fri Jun 28 09:54:06 2024 +0200
+++ b/src/Pure/Build/build_ci.scala	Fri Jun 28 10:58:29 2024 +0200
@@ -88,7 +88,6 @@
     def pre(options: Options, progress: Progress): Unit = ()
     def post(
       options: Options,
-      start_date: Date,
       url: Option[Url],
       results: Build.Results,
       progress: Progress
@@ -161,8 +160,6 @@
     url: Option[Url] = None,
     progress: Progress = new Progress
   ): Unit = {
-    val start_date = Date.now()
-
     def return_code(f: => Unit): Int =
       Exn.capture(f) match {
         case Exn.Res(_) => Process_Result.RC.ok
@@ -192,7 +189,7 @@
         max_jobs = job.hosts.max_jobs)
     }
 
-    val post_result = return_code { job.hook.post(options, start_date, url, results, progress) }
+    val post_result = return_code { job.hook.post(options, url, results, progress) }
 
     val rc = List(mail_result, pre_result, results.rc, post_result).max
     if (rc != Process_Result.RC.ok) {