aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-14 17:50:09 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-14 17:50:09 +0000
commitdfb001fde305a4d3b4e418da39b4075cf55a7f57 (patch)
treea7b52b8f70a33b432559b22d596e005d9b8d0926 /tools
parent4205d7880c264e56b0fc93ae7701cce956838197 (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.ml47
-rw-r--r--tools/coqdep.ml7
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