no more "completed in ."

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 73a4d668f7b381dcc8630a9c434743e0a10cae7f..47447e49eb77268cc2bfc13dfa5fbcea1fd927bf 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -180,9 +180,7 @@ let main ~mode =
      with End_of_file -> ());
     let elapsed = Unix.time () -. time in
     let tm = Unix.gmtime elapsed in
-    let sec = 
-      if tm.Unix.tm_sec > 0 then (string_of_int tm.Unix.tm_sec ^ "''") else "" 
-    in
+    let sec = string_of_int tm.Unix.tm_sec ^ "''" in
     let min = 
       if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else "" 
     in