Merge PR #7575: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.

3 files changed, 5 insertions, 5 deletions

diff --git a/META.coq b/META.coq
index 12d7666cb0..8d4c3d5f00 100644
--- a/META.coq
+++ b/META.coq
@@ -57,9 +57,6 @@ package "vm" (
 # We currently prefer static linking of the VM.
   archive(byte)    = "libcoqrun.a"
   linkopts(byte)   = "-custom"
-
-  linkopts(native) = "-cclib -lcoqrun"
-
 )
 
 package "kernel" (
diff --git a/Makefile.build b/Makefile.build
index 1326027caa..7454e1b0c0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -397,7 +397,6 @@ $(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
-	                   -I kernel/byterun/ -cclib -lcoqrun \
 			   $(SYSMOD) -package camlp5.gramlib \
 			   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP) $@
@@ -637,6 +636,11 @@ kernel/kernel.cma: kernel/kernel.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
+# Specific rule for kernel.cmxa as to adjoin -cclib -lcoqrun
+kernel/kernel.cmxa: kernel/kernel.mllib
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -I kernel/byterun/ -cclib -lcoqrun -a -o $@ $(filter-out %.mllib, $^)
+
 %.cma: %.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
diff --git a/Makefile.ide b/Makefile.ide
index 37f698e0c9..48b5549120 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -147,7 +147,6 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
 $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide \
-	                   -I kernel/byterun/ -cclib -lcoqrun \
 			   $(SYSMOD) -package camlp5.gramlib \
 			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP) $@