aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/tQueue.mli
diff options
context:
space:
mode:
authorGravatar Alec Faithfull <alef@itu.dk>2015-10-06 14:19:34 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-09 11:01:43 +0200
commit56ca108e63191e90c3d4169c37a4c97017e3c6ae (patch)
tree7f2e6e23ed8093d43ec3179980dcfaf5464eebc1 /stm/tQueue.mli
parentce0c536b4430711db1e30cd7ac35ae8d71d34e64 (diff)
TQueue: Expose the length of TQueues
Diffstat (limited to 'stm/tQueue.mli')
-rw-r--r--stm/tQueue.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 7458de510..f54af4df4 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -28,3 +28,5 @@ exception BeingDestroyed
(* Threads blocked in pop can get this exception if the queue is being
* destroyed *)
val destroy : 'a t -> unit
+
+val length : 'a t -> int