aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/main.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 872903e6a5..98204a856d 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -134,7 +134,7 @@ let add_path dir name =
(* turn A/B/C into A.B.C *)
let rec name_of_path p name dirname suffix =
- if p = dirname then String.concat "." (name::suffix)
+ if p = dirname then String.concat "." (if name = "" then suffix else (name::suffix))
else
let subdir = Filename.dirname dirname in
if subdir = dirname then raise Not_found