aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/CoqMakefile.in
diff options
context:
space:
mode:
Diffstat (limited to 'tools/CoqMakefile.in')
-rw-r--r--tools/CoqMakefile.in12
1 files changed, 9 insertions, 3 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fc8c450ec..e919db4a9 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -592,9 +592,14 @@ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
-$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
$(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $<
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ -shared -linkall -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+ $(SHOW)'CAMLOPT -a -o $@'
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
$(SHOW)'CAMLC -a -o $@'
@@ -611,7 +616,8 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
# This rule is for _CoqProject with no .mllib nor .mlpack
$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $<
+ $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ -shared -o $@ $<
ifneq (,$(TIMING))
TIMING_EXTRA = > $<.$(TIMING_EXT)