# HG changeset patch
# User wenzelm
# Date 1457529856 -3600
# Node ID 3541bc1e97d2fc0021cd2a1615d5a6a1bfbcf617
# Parent  cb4e6ca065052956c14bd3b6f4b92d839bfa83b9
elapsed time in milliseconds (cf. Time.now in Poly/ML);

diff -r cb4e6ca06505 -r 3541bc1e97d2 Admin/bash_process/bash_process.c
--- a/Admin/bash_process/bash_process.c	Wed Mar 09 13:33:21 2016 +0100
+++ b/Admin/bash_process/bash_process.c	Wed Mar 09 14:24:16 2016 +0100
@@ -20,6 +20,17 @@
   exit(2);
 }
 
+static time_t now()
+{
+  struct timeval tv;
+  if (gettimeofday(&tv, NULL) == 0) {
+    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+  }
+  else {
+    return time(NULL) * 1000;
+  }
+}
+
 
 int main(int argc, char *argv[])
 {
@@ -36,7 +47,7 @@
 
   /* potential fork */
 
-  time_t time_start = time(NULL);
+  time_t time_start = now();
 
   if (strlen(timing_name) > 0 || setsid() == -1) {
     pid_t pid = fork();
@@ -52,7 +63,7 @@
       /* report timing */
 
       if (strlen(timing_name) > 0) {
-        long long timing_elapsed = (time(NULL) - time_start) * 1000;
+        long long timing_elapsed = now() - time_start;
 
         struct rusage ru;
         getrusage(RUSAGE_CHILDREN, &ru);