diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 87ddb2a95..cc34a355a 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -80,7 +80,8 @@ val stat : string -> stats val read_file : string -> Buffer.t -> unit -(** Read the available content on some gtk asynchronous input channel *) +(** Read what is available on a gtk input channel. + This channel should have been set as non-blocking. *) val io_read_all : Glib.Io.channel -> string |