From 95e60e7769f8fcf25e44774b78a4be17b7e4fb3c Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 2 Sep 2011 15:59:17 +0000
Subject: Coq_makefile: bugfix in install rule

Files in a -I path are now installed in every root directory of -R pathes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14445 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/project_file.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index d543961503..dbfa16e595 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -61,7 +61,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
   | ("-I"|"-custom") :: _ ->
     raise Parsing_error
   | "-f" :: file :: r ->
-    let file = Minilib.correct_path file orig_dir in
+    let file = Minilib.remove_path_dot (Minilib.correct_path file orig_dir) in
     let () = match project_file with
       | None -> ()
       | Some _ -> Minilib.safe_prerr_endline
-- 
cgit v1.2.3