diff options
| author | Pierre-Marie Pédrot | 2020-04-15 19:16:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-26 14:24:48 +0200 |
| commit | e16aab42641f0b79827c4598bf065b1607a08c43 (patch) | |
| tree | 3c184a7c68b8deb4f4ea07e02b5eae91056c8947 | |
| parent | 3dc9ec53041b4b34a601c2d454d0e47005561b30 (diff) | |
Tweak a comment on the low-level objfile API.
| -rw-r--r-- | lib/objFile.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/objFile.mli b/lib/objFile.mli index 36db7f4208..b15b04ee54 100644 --- a/lib/objFile.mli +++ b/lib/objFile.mli @@ -30,5 +30,8 @@ val open_out : file:string -> out_handle val close_out : out_handle -> unit val marshal_out_segment : out_handle -> segment:string -> 'a -> unit val marshal_out_binary : out_handle -> segment:string -> out_channel * (unit -> unit) -(** Low-level API. This function returns a channel and a closure. The channel - should only be written to, and once done, the closure should be invoked. *) +(** [marshal_out_binary oh segment] is a low level, stateful, API returning + [oc, stop]. Once called no other API can be used on the same [oh] and only + [Stdlib.output_*] APIs should be used on [oc]. [stop ()] must be invoked in + order to signal that all data was written to [oc] (which should not be used + afterwards). Only after calling [stop] the other API can be used on [oh]. *) |