diff options
| author | Maxime Dénès | 2015-02-26 14:33:07 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-02-26 14:34:46 +0100 |
| commit | f712a0523359d5b54b4d4160bc77271fdde094a3 (patch) | |
| tree | 1408eabb7d2cb58117a3a82fe2ce2161470c9f05 | |
| parent | c8944dccb081c79eb47ca91c7e2cb5c50558aeaa (diff) | |
Mention -R option in warnings, fixing #4067 and #4068.
| -rw-r--r-- | tools/coq_makefile.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index b84d15d62e..bd78fe2c54 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -48,7 +48,8 @@ let usage () = coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command] - ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value] + ... [-I dir] ... [-R physicalpath logicalpath] + ... [-Q physicalpath logicalpath] ... [VARIABLE = value] ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] [-h] [--help] @@ -767,10 +768,10 @@ let check_overlapping_include (_,inc_i,inc_r) = | [] -> () | (pdir,_,abspdir)::l -> if not (is_prefix pwd abspdir) then - Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir; + Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir; List.iter (fun (pdir',_,abspdir') -> if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then - Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; + Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l; in aux (inc_i@inc_r) let do_makefile args = |