Coq_makefile: -extra[-phony] correction + doc

2 files changed, 21 insertions, 9 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
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 5914ea0e27..9aac367b06 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -48,18 +48,26 @@ let section s =
 let usage () =
   output_string stderr "Usage summary:
 
-coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib]
-  ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath
-  logicalpath] ... [VARIABLE = value] ...  [-arg opt] ... [-opt|-byte]
-  [-no-install] [-f file] [-o file] [-h] [--help]
+coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
+  [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command]
+  ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value]
+  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
+  [-h] [--help]
 
 [file.v]: Coq file to be compiled
 [file.ml[i4]?]: Objective Caml file to be compiled
-[file.mllib]: ocamlbuild file that describes a Objective Caml library
+[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml
+  library/module
 [subdirectory] : subdirectory that should be \"made\" and has a
   Makefile itself to do so.
-[-custom command dependencies file]: add target \"file\" with command
-  \"command\" and dependencies \"dependencies\"
+[-extra result dependencies command]: add target \"result\" with command
+  \"command\" and dependencies \"dependencies\". If \"result\" is not
+  generic (do not contains a %), \"result\" is built by _make all_ and
+  deleted by _make clean_.
+[-extra-phony result dependencies command]: add a PHONY target \"result\"
+ with command \"command\" and dependencies \"dependencies\". Note that
+ _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as
+ as a dependencies of an already defined target \"foo\".
 [-I dir]: look for Objective Caml dependencies in \"dir\"
 [-R physicalpath logicalpath]: look for Coq dependencies resursively
   starting from \"physicalpath\". The logical path associated to the
@@ -642,7 +650,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
 
 let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
   let other_targets = CList.map_filter
-    (fun (n,_,is_phony,_) -> if is_phony || not (is_genrule n) then Some n else None)
+    (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None)
     sps @ sds in
   main_targets vfiles mlfiles other_targets inc;
     print ".PHONY: ";