diff options
Diffstat (limited to 'otherlibs/unix/unix.mli')
| -rw-r--r-- | otherlibs/unix/unix.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/otherlibs/unix/unix.mli b/otherlibs/unix/unix.mli index daa3c9d9d..6f68c9a73 100644 --- a/otherlibs/unix/unix.mli +++ b/otherlibs/unix/unix.mli @@ -349,6 +349,9 @@ val fstat : file_descr -> stats (** Return the informations for the file associated with the given descriptor. *) +val isatty : file_descr -> bool +(** Return [true] if the given file descriptor refers to a terminal or + console window, [false] otherwise. *) (** {6 File operations on large files} *) |