diff options
| author | Maxime Dénès | 2017-05-02 16:04:50 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-02 16:04:50 +0200 |
| commit | 28accc370aa2f6fafbf50b69be7ae5dc06104212 (patch) | |
| tree | 7764de5a598390e9906f064170a480cfcfe0a38d /lib/cErrors.ml | |
| parent | 63503b99c46b27009e85e5c0fa9588b7424a589d (diff) | |
| parent | 9a48211ea8439a8502145e508b70ede9b5929b2f (diff) | |
Merge PR#582: Fix warnings
Diffstat (limited to 'lib/cErrors.ml')
| -rw-r--r-- | lib/cErrors.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1c1ff7e2fd..b55fd80c68 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -121,12 +121,14 @@ end by inner functions during a [vernacinterp]. They should be handled only at the very end of interp, to be displayed to the user. *) +[@@@ocaml.warning "-52"] let noncritical = function | Sys.Break | Out_of_memory | Stack_overflow | Assert_failure _ | Match_failure _ | Anomaly _ | Timeout | Drop | Quit -> false | Invalid_argument "equal: functional value" -> false | _ -> true +[@@@ocaml.warning "+52"] (** Check whether an exception is handled *) |