diff options
Diffstat (limited to 'stm/asyncTaskQueue.mli')
| -rw-r--r-- | stm/asyncTaskQueue.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index a9a215acc8..ea438f3f76 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -68,10 +68,10 @@ module type Task = sig type request type response - (** UID of the task kind, for -toploop *) + (** UID of the task kind *) val name : string ref - (** Extra arguments of the task kind, for -toploop *) + (** Extra arguments of the task kind *) val extra_env : unit -> string array (** {5 Master API, it is run by the master, on a thread} *) |