diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-10 09:45:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-10 09:45:21 +0200 |
| commit | a19746f2ff7933f0b78ecfcd78e3237ef721977a (patch) | |
| tree | 6e2bb24cac2f4d9efe589507810b2558d5cbd0d6 /clib/cList.mli | |
| parent | 51a56b1aacb516af513de64c00dd7e796f661484 (diff) | |
[lib] Fix wrong deprecation comment.
Diffstat (limited to 'clib/cList.mli')
| -rw-r--r-- | clib/cList.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/clib/cList.mli b/clib/cList.mli index d080ebca2..13e069e94 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -354,7 +354,7 @@ sig (** [subtract] specialized to physical equality *) val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list - (** [@@ocaml.deprecated "Same as [merge_set]"] *) + [@@ocaml.deprecated "Same as [merge_set]"] (** {6 Uniqueness and duplication} *) |