From 55d286505c5b55fe73cc1587797fe023581f109e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicol=C3=A1s=20Ojeda=20B=C3=A4r?= Date: Sun, 29 Dec 2019 09:55:13 -0800 Subject: Merge pull request #9217 from kit-ty-kate/fix-doc-filename-null Add missing since annotation for Filename.null (cherry picked from commit bb62942ed5c3081d295e0b78a1c16cfb9061b613) --- stdlib/filename.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/stdlib/filename.mli b/stdlib/filename.mli index 9e032b8625..1e77c0d863 100644 --- a/stdlib/filename.mli +++ b/stdlib/filename.mli @@ -120,7 +120,9 @@ val dirname : string -> string val null : string (** [null] is ["/dev/null"] on POSIX and ["NUL"] on Windows. It represents a - file on the OS that discards all writes and returns end of file on reads. *) + file on the OS that discards all writes and returns end of file on reads. + + @since 4.10.0 *) val temp_file : ?temp_dir: string -> string -> string -> string (** [temp_file prefix suffix] returns the name of a -- cgit v1.2.1