coq_makefile logical path ending with '.' are correctly convert to physical path

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14272 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 4 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 71fe04fa7..73e2325c9 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -123,8 +123,9 @@ let has_top_file = function
   | _ -> false
 
 let physical_dir_of_logical_dir ldir =
-  let pdir = String.copy ldir in
-  for i = 0 to String.length ldir - 1 do
+  let le = String.length ldir - 1 in
+  let pdir = if ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in
+  for i = 0 to le - 1 do
     if pdir.[i] = '.' then pdir.[i] <- '/';
   done;
   pdir
@@ -198,12 +199,14 @@ let install_doc some_vfiles some_mlifiles (_,inc_r) =
 	  if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)";
       |(_,lp,_)::q ->
 	 let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
-	   if (pr <> "") && ((lp = pr) || pr.[String.length pr - 1] = '.') then begin
+	   if (pr <> "") &&
+	     ((List.exists (fun(_,b,_) -> b = pr) inc_r) || pr.[String.length pr - 1] = '.')
+	   then begin
 	     let rt = physical_dir_of_logical_dir pr in
 	       if some_vfiles then install_one_kind "html" rt;
 	       if some_mlifiles then install_one_kind "mlihtml" rt;
 	   end else begin
-	     prerr_string "Warning: -R options don't have a correct common preffix,
+	     prerr_string "Warning: -R options don't have a correct common prefix,
  install-doc will put anything in $INSTALLDEFAULTROOT";
 	   if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)";
 	   if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)";