From 7534ae80c65f151030c7017c11d30eaa46af453e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 18 Jan 2016 18:25:11 +0100
Subject: [PATCH] comment in shuffle
---
src/util/shuffle.mli | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/util/shuffle.mli b/src/util/shuffle.mli
index 8de61a2ec..71eb1e3f4 100644
--- a/src/util/shuffle.mli
+++ b/src/util/shuffle.mli
@@ -1,4 +1,3 @@
-
val set_shuffle: int array option -> unit
(** if None is given shuffling is disable (default) *)
@@ -23,5 +22,8 @@ val seql': ('a -> unit) -> 'a list -> unit
val seql : (unit -> unit) list -> unit
val chooseb: ('a -> 'b) -> ((unit -> bool) ->'a -> 'b) -> 'a -> 'b
+(** [chooseb f g] call f if there is no shuffling or g otherwise.
+ The first argument given to g is a random boolean generator.
+*)
val int: int -> int
--
GitLab