coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs

7 files changed, 14 insertions, 5 deletions

diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 1feff7479b..dc5a500db8 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
 ./test
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.glob
 ./test/test.v
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 1feff7479b..dc5a500db8 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
 ./test
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.glob
 ./test/test.v
diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local
index 5373b0219f..0f4a7d9954 100644
--- a/test-suite/coq-makefile/findlib-package/Makefile.local
+++ b/test-suite/coq-makefile/findlib-package/Makefile.local
@@ -1,3 +1 @@
 CAMLPKGS   += -package foo
-CAMLLINK    := "$(OCAMLFIND)" ocamlc   -rectypes -thread -linkpkg -dontlink str
-CAMLOPTLINK := "$(OCAMLFIND)" ocamlopt -rectypes -thread -linkpkg -dontlink str
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 51669f28f5..03df9cf050 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 51669f28f5..03df9cf050 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 3bec11cb75..89bafe9ad1 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -18,6 +18,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fc8c450ec8..e919db4a98 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)