From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Dec 2005 14:02:20 +0000 (+0000)
Subject: no more "completed in ."
X-Git-Tag: make_still_working~7977
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=86671ef183faa0ff4731d06d69349689fa4c084c;p=helm.git

no more "completed in ."
---

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 73a4d668f..47447e49e 100644
--- 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