diff options
Diffstat (limited to 'otherlibs/unix/unixLabels.mli')
| -rw-r--r-- | otherlibs/unix/unixLabels.mli | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/otherlibs/unix/unixLabels.mli b/otherlibs/unix/unixLabels.mli index 3ab7e6289..1f081c81f 100644 --- a/otherlibs/unix/unixLabels.mli +++ b/otherlibs/unix/unixLabels.mli @@ -263,7 +263,15 @@ val write : file_descr -> buf:string -> pos:int -> len:int -> int (** [write fd buff ofs len] writes [len] characters to descriptor [fd], taking them from string [buff], starting at position [ofs] in string [buff]. Return the number of characters actually - written. *) + written. + + When an error is reported some characters might have already been + written. Use [single_write] instead to ensure that this is not the + case. *) + +val single_write : file_descr -> buf:string -> pos:int -> len:int -> int +(** Same as [write] but ensures that all errors are reported and + that no character has ever been written when an error is reported. *) (** {6 Interfacing with the standard input/output library} *) |