switch off profilers

[helm.git] / helm / software / components / extlib / hExtlib.ml

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 3ee270e4e00b42fd0b012a512b11a92feef48c82..c2de58f810fe99728b5b13253135c12934e02bec 100644 (file)
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -27,7 +27,7 @@
 
 (** PROFILING *)
 
-let profiling_enabled = false ;; (* ComponentsConf.profiling *)
+let profiling_enabled = ref false ;; (* ComponentsConf.profiling *)
 
 let something_profiled = ref false
 
@@ -47,11 +47,12 @@ let set_profiling_printings f = profiling_printings := f
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
 let profile ?(enable = true) s =
- if profiling_enabled && enable then
+ if !profiling_enabled && enable then
    let total = ref 0.0 in
    let calls = ref 0 in
    let max = ref 0.0 in
    let profile f x =
+    if not !profiling_enabled then f x else
     let before = Unix.gettimeofday () in
     try
      incr calls;
@@ -444,7 +445,7 @@ let find_in paths path =
        try
          if (Unix.stat path).Unix.st_kind = Unix.S_REG then path
          else aux tl
-       with Unix.Unix_error _ as exn -> 
+       with Unix.Unix_error _ -> 
                aux tl
    in
    try