From dd710b9adbe7b27dccd6d4b21b90cb9bd07e5c07 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 26 Dec 2016 10:02:34 +0100 Subject: Fix some documentation typos. --- lib/profile.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/profile.ml b/lib/profile.ml index 2350cd43ac..13c2d9c802 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. @@ -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