diff options
Diffstat (limited to 'lib/profile.ml')
| -rw-r--r-- | lib/profile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/profile.ml b/lib/profile.ml index 2350cd43a..0910db3fe 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -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 |