diff options
author | 2008-03-14 17:50:09 +0000 | |
---|---|---|
committer | 2008-03-14 17:50:09 +0000 | |
commit | dfb001fde305a4d3b4e418da39b4075cf55a7f57 (patch) | |
tree | a7b52b8f70a33b432559b22d596e005d9b8d0926 /tools | |
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')
-rw-r--r-- | tools/coq_makefile.ml4 | 7 | ||||
-rw-r--r-- | tools/coqdep.ml | 7 |
2 files changed, 8 insertions, 6 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 8e3e0aa45..9b95bf7cd 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -138,10 +138,9 @@ let implicit () = print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html $< -o $@\n\n"; print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n"; - print "%.v.d.raw: %.v\n"; - print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\"\\\n\t || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; - print "%.v.d: %.v.d.raw\n"; - print "\t$(HIDE)sed 's/\\(.*\\)\\.vo[[:space:]]*:/\\1.vo \\1.glob:/' < \"$<\" > \"$@\" \\\n\t || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + print "%.v.d: %.v\n"; + print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + and ml_suffixes = if !some_mlfile then [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ] diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 35608cd64..2ce73cef2 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 |