From 534b8afafc763b382fb3fa747bb95a9a57676d4c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 9 Aug 2017 14:43:48 +0200
Subject: coq_makefile: build/use .cma for packed plugins

The build chain is always

ml -> cmo -> cma
ml -> cmx -> cmxa -> cmxs

If we are packing, then it becomes

ml -> cmo \
ml -> cmo --> cmo -> cma
ml -> cmo /

ml -> cmxo \
ml -> cmxo --> cmxo -> cmxa -> cmxs
ml -> cmxo /

The interest of always having a .cma or .cmxa is that such file can
carry linking flags, that in findlib terms means which
-package was use to build the plugin.
---
 tools/CoqMakefile.in | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 9f891afe53..f6fe6ddeb1 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -151,7 +151,7 @@ OPT?=
 # The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
 ifeq '$(OPT)' '-byte'
 USEBYTE:=true
-DYNOBJ:=.cmo
+DYNOBJ:=.cma
 DYNLIB:=.cma
 else
 USEBYTE:=
-- 
cgit v1.2.3