aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-10-09 12:59:41 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-10-09 13:19:58 +0200
commit2d5b39132f4a7dd2541f95d795682089eb1c5f5e (patch)
tree494e47eefd292e8321fa4ca0f2a7fb6095a65be2
parente294b5dec7a36c758a36b18e90fc27bce4a6f441 (diff)
Fixup leading ./ path cleaning
-rw-r--r--lib/cUnix.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/cUnix.ml b/lib/cUnix.ml
index a4d6903c0..55d888ef2 100644
--- a/lib/cUnix.ml
+++ b/lib/cUnix.ml
@@ -34,10 +34,12 @@ let rec cut_after_dirsep p pos =
else
String.sub p pos (String.length p - pos)
-(** remove all initial "./" in a path *)
+(** remove all initial "./" in a path unless the path is exactly "./" *)
let rec remove_path_dot p =
if CString.is_sub curdir p 0 then
- remove_path_dot (cut_after_dirsep p curdir_len)
+ if String.length p = curdir_len
+ then Filename.current_dir_name
+ else remove_path_dot (cut_after_dirsep p curdir_len)
else
p