diff options
| author | pboutill | 2011-09-01 09:51:31 +0000 |
|---|---|---|
| committer | pboutill | 2011-09-01 09:51:31 +0000 |
| commit | 02c63cbf0c7ee8feacea68b39ceaebdce69c4af8 (patch) | |
| tree | 7b002fb7dc79b03e4015edc50905630a0cb06818 /tools | |
| parent | d122799af45e81608a40063568e9f4b6d6deec33 (diff) | |
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
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |