Actually fix time options to get time in secs

ncough · Nov 10, 2017 · ab16f20 · ab16f20
1 parent 9a9711c
commit ab16f20
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/worker.sml b/worker.sml
@@ -242,7 +242,7 @@ end
 
 local
   val resume_file = "resume"
-  val time_options = String.concat["--format='%E %M' --output='",timing_file,"'"]
+  val time_options = String.concat["--format='%e %M' --output='",timing_file,"'"]
   val max_dir_length = 50
   fun pad dir =
     let