diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-04 19:47:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-23 02:35:58 +0100 |
| commit | 19a584d3fa9594abdf3dcc0148f368547ce77ccc (patch) | |
| tree | 4888e4e7fe950382c6e635e9854d9d1790527fdd /lib/coqProject_file.ml4 | |
| parent | 143244e0606a790b73da2360fb0eabe3d98d4b4e (diff) | |
Forbidding -o and -f in input file of coq_makefile.
This was apparently either silently doing nothing or failing.
Diffstat (limited to 'lib/coqProject_file.ml4')
| -rw-r--r-- | lib/coqProject_file.ml4 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 970666638..34f9aed37 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -113,6 +113,7 @@ let exists_dir dir = let process_cmd_line orig_dir proj args = + let parsing_project_file = ref (proj.project_file <> None) in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in @@ -155,16 +156,22 @@ let process_cmd_line orig_dir proj args = aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r | "-f" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file)); let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () | Some _ -> Feedback.msg_warning (Pp.str "Multiple project files are deprecated.") in + parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in + parsing_project_file := false; aux proj r | "-o" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file)); if String.contains file '/' then error "Output file must be in the current directory"; if proj.makefile <> None then |