aboutsummaryrefslogtreecommitdiff
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
authorPierre Letouzey2016-06-15 12:48:26 +0200
committerPierre Letouzey2016-06-15 13:04:44 +0200
commit3e0f94ac02fac8f4693e51b6656f9448b4b50921 (patch)
tree38f21757c0db967f006eeb907cfe57ba7f54420e /tools/coqdep_common.ml
parent2861a39461c6e13f701892af84c7beebfb8f4215 (diff)
ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpack
Since we already have a rule %.cmxs:%.cmxa and the .cmxa depends already on all the .cmx inside it, no need to state explicitely that the .cmxs depends on these inner .cmx. Same thing concerning .cmxs built out of a single .cmx.
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0f7937d729..cc63c13d7b 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -445,7 +445,7 @@ let mL_dependencies () =
let efullname = escape fullname in
printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
- printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname;
+ printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
flush stdout)
(List.rev !mllibAccu);
List.iter
@@ -455,7 +455,7 @@ let mL_dependencies () =
let efullname = escape fullname in
printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep;
printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
- printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname efullname;
+ printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
flush stdout)
(List.rev !mlpackAccu)