diff options
Diffstat (limited to 'stm/tQueue.ml')
| -rw-r--r-- | stm/tQueue.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/tQueue.ml b/stm/tQueue.ml index a0b08778b..fee4f35b4 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -88,7 +88,7 @@ let broadcast { lock = m; cond = c } = let push { queue = q; lock = m; cond = c; release } x = if release then CErrors.anomaly(Pp.str - "TQueue.push while being destroyed! Only 1 producer/destroyer allowed"); + "TQueue.push while being destroyed! Only 1 producer/destroyer allowed."); Mutex.lock m; PriorityQueue.push q x; Condition.broadcast c; |