From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 1 Jun 2007 19:32:06 +0000 (+0000)
Subject: Profiling enabled again.
X-Git-Tag: make_still_working~6259
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a1a8ac61970fce48a3e0c8fa673a70a03e026c50;p=helm.git

Profiling enabled again.
---

diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
index 69911cfb3..da4bd3cde 100644
--- a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
@@ -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*)