diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-07 15:16:47 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-07 15:16:47 +0000 |
| commit | fe120f195707e89164a8c28c9fdd995c9d0f1231 (patch) | |
| tree | fcc2559f526e99715c55b8d16c4d14fa9831e6cd | |
| parent | c0543e34982b837c228232350febb8b30673a848 (diff) | |
coq_makefile doesn't complain anymore when a dir is both -I and -R
It used to deal correctly with that so why a warning ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14269 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tools/coq_makefile.ml4 | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 6e7f8f07f..3ea9ce3a8 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -218,7 +218,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles),_,sds) inc = print "\n"; end; print "install:"; - if (not_empty ml4files) || (not_empty mlfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; + if (not_empty cmfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; print "\n"; if not_empty vfiles then install_include_by_root "COQLIB" "VOFILES" vfiles inc; if (not_empty cmfiles) then begin @@ -634,15 +634,15 @@ let ensure_root_dir l = let warn_install_at_root_directory (vfiles,(mlifiles,ml4files,mlfiles),_,_) (inc_i,inc_r) = let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in - let inc_top = List.map (fun (p,_,a) -> (p,a)) inc_r_top @ inc_i in + let inc_top = List.map (fun (p,_,_) -> p) inc_r_top @ List.map fst inc_i in let files = vfiles @ mlifiles @ ml4files @ mlfiles in if not !no_install && - List.exists (fun f -> List.mem_assoc (Filename.dirname f) inc_top) files + List.exists (fun f -> List.mem (Filename.dirname f) inc_top) files then Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n" (if inc_r_top = [] then "" else "with non trivial logical root ") -let check_overlapping_include (inc_i,inc_r) = +let check_overlapping_include (_,inc_r) = let pwd = Sys.getcwd () in let rec aux = function | [] -> () @@ -652,9 +652,6 @@ let check_overlapping_include (inc_i,inc_r) = List.iter (fun (pdir',_,abspdir') -> if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; - List.iter (fun (pdir',abspdir') -> - if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then - Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i in aux inc_r let do_makefile args = |