From 2bdfddc39d1fd6200042ddb95ded98b44e14b8e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 May 2019 11:24:51 +0200
Subject: Passing command-line option async_proofs_worker_priority
 functionally.

We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".
---
 stm/asyncTaskQueue.mli | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'stm/asyncTaskQueue.mli')

diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index ea438f3f76..e6cf6343c8 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -144,10 +144,10 @@ module MakeQueue(T : Task) () : sig
   (** [queue] is the abstract queue type. *)
   type queue
 
-  (** [create n] will initialize the queue with [n] workers. If [n] is
-      0, the queue won't spawn any process, working in a lazy local
-      manner. [not imposed by the this API] *)
-  val create : int -> queue
+  (** [create n pri] will initialize the queue with [n] workers having
+      priority [pri]. If [n] is 0, the queue won't spawn any process,
+      working in a lazy local manner. [not imposed by the this API] *)
+  val create : int -> CoqworkmgrApi.priority -> queue
 
   (** [destroy q] Deallocates [q], cancelling all pending tasks. *)
   val destroy : queue -> unit
@@ -203,9 +203,9 @@ module MakeQueue(T : Task) () : sig
   (** [clear q] Clears [q], only if the worker prool is empty *)
   val clear : queue -> unit
 
-  (** [with_n_workers n f] create a queue, run the function, destroy
+  (** [with_n_workers n pri f] creates a queue, runs the function, destroys
       the queue. The user should call join *)
-  val with_n_workers : int -> (queue -> 'a) -> 'a
+  val with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a
 
 end
 
-- 
cgit v1.2.3