From 4b5527a6ccbe73ada47f903292959ed3dde3b5c6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Apr 2008 11:59:49 +0000
Subject: [PATCH] allow to switch profiling on and off on the fly

---
 helm/software/components/extlib/hExtlib.ml  | 7 ++++---
 helm/software/components/extlib/hExtlib.mli | 2 ++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 3ee270e4e..0d7254c8b 100644
--- 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 true ;; (* 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
diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 73450ae11..30a6f145f 100644
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -129,3 +129,5 @@ val estimate_size: 'a -> int
 val is_prefix_of: string -> string -> bool
 val chop_prefix: string -> string -> string
 val touch: string -> unit
+
+val profiling_enabled: bool ref
-- 
2.39.2