From 02c63cbf0c7ee8feacea68b39ceaebdce69c4af8 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 1 Sep 2011 09:51:31 +0000
Subject: Coq_makefile : bug when a project file is not in the current
 directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coq_makefile.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index e26abdb3e4..738c1ea2be 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -70,6 +70,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib]
 [-no-install]: build a makefile with no install target
 [-f file]: take the contents of file as arguments
 [-o file]: output should go in file file
+	Output file outside the current directory is forbidden.
 [-h]: print this usage summary
 [--help]: equivalent to [-h]\n";
   exit 1
@@ -551,7 +552,7 @@ let do_makefile args =
     |[] -> var := false
     |_::_ -> var := true in
   let (project_file,makefile,is_install,opt),l =
-    try Project_file.process_cmd_line (None,None,true,true) [] args
+    try Project_file.process_cmd_line Filename.current_dir_name (None,None,true,true) [] args
     with Project_file.Parsing_error -> usage () in
   let (v_f,(mli_f,ml4_f,ml_f,mllib_f),sps,sds as targets), inc, defs =
     Project_file.split_arguments l in
-- 
cgit v1.2.3