From a4779227fa825383075780dff2a7625140cd6ef7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 7 May 2025 13:15:37 -0400 Subject: [PATCH] add .mli for rpool --- src/util/rpool.mli | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 src/util/rpool.mli diff --git a/src/util/rpool.mli b/src/util/rpool.mli new file mode 100644 index 0000000..5998658 --- /dev/null +++ b/src/util/rpool.mli @@ -0,0 +1,10 @@ +(** A resource pool (for buffers) *) + +type 'a t + +val create : + max_size:int -> create:(unit -> 'a) -> clear:('a -> unit) -> unit -> 'a t + +val alloc : 'a t -> 'a +val recycle : 'a t -> 'a -> unit +val with_ : 'a t -> ('a -> 'b) -> 'b