diff options
| author | letouzey | 2008-03-14 17:50:09 +0000 |
|---|---|---|
| committer | letouzey | 2008-03-14 17:50:09 +0000 |
| commit | dfb001fde305a4d3b4e418da39b4075cf55a7f57 (patch) | |
| tree | a7b52b8f70a33b432559b22d596e005d9b8d0926 /tools/coqdep.ml | |
| parent | 4205d7880c264e56b0fc93ae7701cce956838197 (diff) | |
New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10668 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 35608cd640..2ce73cef2c 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -22,6 +22,7 @@ let option_D = ref false let option_w = ref false let option_i = ref false let option_sort = ref false +let option_glob = ref false let option_slash = ref false let suffixe = ref ".vo" @@ -365,11 +366,12 @@ let mL_dependencies () = let coq_dependencies () = List.iter (fun (name,_) -> - printf "%s%s: %s.v" name !suffixe name; + let glob = if !option_glob then " "^name^".glob" else "" in + printf "%s%s%s: %s.v" name !suffixe glob name; traite_fichier_Coq true (name ^ ".v"); printf "\n"; if !option_i then begin - printf "%s%s: %s.v" name !suffixe_spec name; + printf "%s%s%s: %s.v" name !suffixe_spec glob name; traite_fichier_Coq false (name ^ ".v"); printf "\n"; end; @@ -527,6 +529,7 @@ let coqdep () = | "-w" :: ll -> option_w := true; parse ll | "-i" :: ll -> option_i := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll + | "-glob" :: ll -> option_glob := true; parse ll | "-I" :: r :: ll -> add_directory (r, []); parse ll | "-I" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_directory r ln; parse ll |