diff options
| author | coqbot-app[bot] <50967743+coqbot-app[bot]@users.noreply.github.com> | 2021-12-10 14:52:36 (GMT) |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-10 14:52:36 (GMT) |
| commit | 04aef4f3c4eb3e32d18fc5219573a7218fcc5748 (patch) | |
| tree | edc4b3871d67d98c1ed97848148613c9fb8b69d1 /clib | |
| parent | 8797c9435578b9921093e211d4ca57b9dd3a483d (diff) | |
| parent | a58316be5a6d80f7cc28d8143465be6a2989fd9d (diff) | |
| download | coq-04aef4f3c4eb3e32d18fc5219573a7218fcc5748.zip coq-04aef4f3c4eb3e32d18fc5219573a7218fcc5748.tar.gz coq-04aef4f3c4eb3e32d18fc5219573a7218fcc5748.tar.bz2 | |
Merge PR #15293: Drop backtrace when raising Exit
Reviewed-by: Alizter
Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cArray.ml | 2 | ||||
| -rw-r--r-- | clib/option.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/clib/cArray.ml b/clib/cArray.ml index 9ecf72c..093db66 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -457,7 +457,7 @@ let distinct v = try Array.iter (fun x -> - if Hashtbl.mem visited x then raise Exit + if Hashtbl.mem visited x then raise_notrace Exit else Hashtbl.add visited x x) v; true diff --git a/clib/option.ml b/clib/option.ml index d1775ae..5810cbf 100644 --- a/clib/option.ml +++ b/clib/option.ml @@ -210,7 +210,7 @@ module List = | [] -> [] | x :: l -> match f x with - | None -> raise Exit + | None -> raise_notrace Exit | Some y -> y :: aux f l in try Some (aux f l) with Exit -> None |