diff options
-rw-r--r-- | stdlib/filename.ml | 13 | ||||
-rw-r--r-- | stdlib/filename.mli | 5 |
2 files changed, 12 insertions, 6 deletions
diff --git a/stdlib/filename.ml b/stdlib/filename.ml index 7d6887eaf4..afe19611ad 100644 --- a/stdlib/filename.ml +++ b/stdlib/filename.ml @@ -129,11 +129,14 @@ let concat dirname filename = else dirname ^ dir_sep ^ filename let basename name = - try - let p = rindex_dir_sep name + 1 in - String.sub name p (String.length name - p) - with Not_found -> - name + let raw_name = + try + let p = rindex_dir_sep name + 1 in + String.sub name p (String.length name - p) + with Not_found -> + name + in + if raw_name = "" then current_dir_name else raw_name let dirname name = try diff --git a/stdlib/filename.mli b/stdlib/filename.mli index 086775f5e9..ed63a45fd5 100644 --- a/stdlib/filename.mli +++ b/stdlib/filename.mli @@ -60,7 +60,10 @@ val basename : string -> string which is equivalent to [name]. Moreover, after setting the current directory to [dirname name] (with {!Sys.chdir}), references to [basename name] (which is a relative file name) - designate the same file as [name] before the call to {!Sys.chdir}. *) + designate the same file as [name] before the call to {!Sys.chdir}. + + The result is not specified if the argument is not a valid file name + (for example, under Unix if there is a NUL character in the string). *) val dirname : string -> string (** See {!Filename.basename}. *) |