diff options
| author | Hugo Herbelin | 2019-05-10 11:25:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | c41f747f7df49bc26983d41096519672f05b793a (patch) | |
| tree | 2d8c8303f0fc00a59855fa3d7c939b6141fcda99 /stm/asyncTaskQueue.mli | |
| parent | e55ba2f04578738ec72c4ca64daf23b9ea51ec06 (diff) | |
Layout/documentation updates.
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} *) |