From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- lib/profile.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'lib/profile.ml') diff --git a/lib/profile.ml b/lib/profile.ml index 2350cd43..d620fe69 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -146,9 +146,9 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = number of allocated bytes may exceed the maximum integer capacity (2^31 on 32-bits architectures); therefore, allocation is measured by small steps, total allocations are computed by adding elementary - measures and carries are controled from step to step *) + measures and carries are controlled from step to step *) -(* Unix measure of time is approximative and shoitt delays are often +(* Unix measure of time is approximate and short delays are often unperceivable; therefore, total times are measured in one (big) step to avoid rounding errors and to get the best possible approximation. @@ -260,7 +260,7 @@ let time_overhead_B_C () = let _dw = dummy_spent_alloc () in let _dt = get_time () in () - with e when Errors.noncritical e -> assert false + with e when CErrors.noncritical e -> assert false done; let after = get_time () in let beforeloop = get_time () in @@ -358,7 +358,7 @@ let declare_profile name = prof_table := (name,e)::!prof_table; e -(* Default initialisation, may be overriden *) +(* Default initialization, may be overridden *) let _ = init_profile () (******************************) -- cgit v1.2.3