diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-25 14:31:15 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:42:01 +0200 |
| commit | 87910d7be9bd50de4db80f70c6e287c7c7994460 (patch) | |
| tree | ff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /lib/cErrors.ml | |
| parent | 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff) | |
Fix 4.04 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 1c1ff7e2f..b55fd80c6 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 *) |