diff options
Diffstat (limited to 'lib/profile.ml')
| -rw-r--r-- | lib/profile.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 () (******************************) |