]> matita.cs.unibo.it Git - helm.git/commitdiff
Profiling enabled again.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Jun 2007 19:32:06 +0000 (19:32 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Jun 2007 19:32:06 +0000 (19:32 +0000)
matita/contribs/formal_topology/bin/theory_explorer.ml

index 69911cfb356b4bae102ac55c66a7f46dac744b24..da4bd3cdea0818b1110f7f080b5832b18925624e 100644 (file)
@@ -7,7 +7,7 @@ let profile f x =
  let res = f x in
  let after = Unix.gettimeofday () in
  let delta = after -. before in
-  if res = Unix.WEXITED 0 then
+  if res then
    ok_time := !ok_time +. delta
   else
    ko_time := !ko_time +. delta;
@@ -256,7 +256,7 @@ let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
   output_string ch (query ^ "\n");
   close_out ch;
 *)
-  let res = exec_cmds [query1; query2; query3; query4] in
+  let res = profile exec_cmds [query1; query2; query3; query4] in
 (*
   let res =
    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)