diff options
| author | Hugo Herbelin | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:21:58 +0200 |
| commit | 34237bb07fa8663d3d9e8ca4f9459f46841fd43d (patch) | |
| tree | bb514dfb7bd2e432264e5c7c502cfc2566df31a2 /clib | |
| parent | 023d189aa201c8d5c71bc7de3e98725273d01b4f (diff) | |
Search: Displaying the "use About" notice only when really needed.
Diffstat (limited to 'clib')
| -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 07f42770f9..c8e471f989 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -265,7 +265,7 @@ sig This is the second part of [chop]. *) val skipn_at_least : int -> 'a list -> 'a list - (** Same as [skipn] but returns [] if [n] is larger than the list of + (** Same as [skipn] but returns [] if [n] is larger than the length of the list. *) val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list |