summaryrefslogtreecommitdiff
path: root/src/util.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/util.mli')
-rw-r--r--src/util.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util.mli b/src/util.mli
index 15ddfef0..38af1fc2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -218,3 +218,5 @@ val split_on_char : char -> string -> string list
val is_some : 'a option -> bool
val is_none : 'a option -> bool
+
+val take : int -> 'a list -> 'a list