# HG changeset patch
# User wenzelm
# Date 1678287463 -3600
# Node ID 066d5df144f044b10e4667304c5b8ef1d7565aa6
# Parent  8036d5f129971aa9664275daa068ad6b326a82e5
assume total operation: ProcessHandle.current().info.startInstant appears to work on all platforms;

diff -r 8036d5f12997 -r 066d5df144f0 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 15:50:29 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 15:57:43 2023 +0100
@@ -164,7 +164,7 @@
     build_uuid: String,
     hostname: String,
     java_pid: Long,
-    java_start: Option[Date],
+    java_start: Date,
     start: Date,
     stamp: Date,
     stop: Option[Date],
@@ -480,7 +480,7 @@
               build_uuid = res.string(Workers.build_uuid),
               hostname = res.string(Workers.hostname),
               java_pid = res.long(Workers.java_pid),
-              java_start = res.get_date(Workers.java_start),
+              java_start = res.date(Workers.java_start),
               start = res.date(Workers.start),
               stamp = res.date(Workers.stamp),
               stop = res.get_date(Workers.stop),
@@ -500,7 +500,7 @@
       build_uuid: String,
       hostname: String,
       java_pid: Long,
-      java_start: Option[Date]
+      java_start: Date
     ): Long = {
       def err(msg: String): Nothing =
         error("Cannot start worker " + worker_uuid + if_proper(msg, "\n" + msg))
@@ -937,8 +937,7 @@
     for (db <- _database) {
       val java = ProcessHandle.current()
       val java_pid = java.pid
-      val java_start0 = java.info.startInstant
-      val java_start = if (java_start0.isPresent) Some(Date.instant(java_start0.get)) else None
+      val java_start = Date.instant(java.info.startInstant.get)
       val serial =
         Build_Process.Data.start_worker(
           db, worker_uuid, build_uuid, build_context.hostname, java_pid, java_start)