diff options
| author | Guillaume Melquiond | 2016-12-26 10:02:34 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-12-26 10:11:41 +0100 |
| commit | dd710b9adbe7b27dccd6d4b21b90cb9bd07e5c07 (patch) | |
| tree | 2953abfc518b395a67634f71ab483516e3324e8b /lib | |
| parent | 827370fb97c138c16509bd549eaeddf94ca13c99 (diff) | |
Fix some documentation typos.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/profile.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 () (******************************) |