From 72f4c53c7d74a971ae89a9c2ae42d9265f39fcd4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Mar 2006 16:21:45 +0000 Subject: [PATCH] Profiling code for merge_ugraphs commented out (since profiling is much more expensive than the profiled code). --- components/cic/cicUniv.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml index 8ae118c9b..b77830954 100644 --- a/components/cic/cicUniv.ml +++ b/components/cic/cicUniv.ml @@ -600,10 +600,13 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = fst (merge_brutal increment base_ugraph), UriManager.UriSet.add uri_of_increment already_contained -let profiler_merge = HExtlib.profile "CicUniv.merge_graphs" +(* profiling code; WARNING: the time spent during profiling can be + greater than the profiled time +let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs" let merge_ugraphs ~base_ugraph ~increment = profiler_merge.HExtlib.profile (fun _ -> merge_ugraphs ~base_ugraph ~increment) () +*) (*****************************************************************************) (** Xml sesialization and parsing **) -- 2.39.2