From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Apr 2008 12:04:09 +0000 (+0000)
Subject: added profiling on/off
X-Git-Tag: make_still_working~5383
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=805758c883a9bd9320942b310af8786ddb7f01b8;p=helm.git

added profiling on/off
---

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 4dd6fcbf4..e98010de9 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -41,6 +41,7 @@ let _ =
       -> None) alluris 
   in
   prerr_endline "caching objects";
+  HExtlib.profiling_enabled := false;
   List.iter (fun uu ->
      indent := 0;
 (*     prerr_endline ("************* INIZIO **************** " ^ NUri.string_of_uri uu); *)
@@ -59,6 +60,7 @@ let _ =
     alluris;
   NCicEnvironment.invalidate ();
   Gc.compact ();
+  HExtlib.profiling_enabled := true;
   prerr_endline "typechecking, first with the new and then with the old kernel";
   let prima = Unix.gettimeofday () in
   List.iter