aboutsummaryrefslogtreecommitdiff
path: root/clib
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-07 11:09:35 +0100
committerMaxime Dénès2018-03-07 11:09:35 +0100
commit5a2e1b95411376206f23046991e1ae5e8a259f01 (patch)
tree91da1aa086f63a0fa5318af282cc77b6d979a0f3 /clib
parent719a10381a7738f82ef5d6abc3d19accf99ad4f0 (diff)
parent65701510e61651c91d4c256c04499cc3cf38794c (diff)
Merge PR #6905: Fix make ml-doc
Diffstat (limited to 'clib')
-rw-r--r--clib/option.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/clib/option.ml b/clib/option.ml
index c2e2e70970..21913e8f7a 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -44,7 +44,7 @@ let hash f = function
exception IsNone
(** [get x] returns [y] where [x] is [Some y].
- @raise [IsNone] if [x] equals [None]. *)
+ @raise IsNone if [x] equals [None]. *)
let get = function
| Some y -> y
| _ -> raise IsNone