From ba5c1c83e77e701ef11625687ec27931bc4bb944 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Apr 2008 15:22:03 +0000 Subject: [PATCH] switch off profilers --- helm/software/components/extlib/hExtlib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 0d7254c8b..c2de58f81 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -27,7 +27,7 @@ (** PROFILING *) -let profiling_enabled = ref true ;; (* ComponentsConf.profiling *) +let profiling_enabled = ref false ;; (* ComponentsConf.profiling *) let something_profiled = ref false -- 2.39.2