diff options
| author | Pierre Boutillier | 2014-06-12 15:27:02 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-06-30 09:49:44 +0200 |
| commit | 8e3ef4dbfd00c67af1cc2b83307038a6440584cb (patch) | |
| tree | a2ce2902e4112ae384175c1f71e229039ffe7be5 /ide | |
| parent | a273df3af0e4315fd792efd83b9365320531111d (diff) | |
Coq_makefile: -extra[-phony] correction + doc
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/project_file.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 44bf12828c..28df1fca3c 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -71,6 +71,10 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) in process_cmd_line orig_dir (project_file,makefile,install,opt) l r | "-custom" :: com :: dependencies :: file :: r -> + Pp.msg_warning (Pp.app + (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".") + (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.") + ); process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r | "-extra" :: file :: dependencies :: com :: r -> process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r @@ -80,7 +84,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir)) :: l) r | "-R" :: p :: lp :: r -> process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r - | ("-I"|"-custom") :: _ -> + | ("-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> raise Parsing_error | "-f" :: file :: r -> let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in |