aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-02-14 15:09:42 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-02-14 18:50:58 +0100
commit9c5db70b891bf6c3e173a31d4e8761e586c7814a (patch)
treee5fd8138b5c9168b2b6ab3174aa8a127797fdf7c /Makefile.common
parent93862f2ab93ec3fab3549c868706bc247422674b (diff)
Makefile: in byte we can always dynlink
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common9
1 files changed, 9 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common
index d752a5be9..e54861961 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -207,12 +207,21 @@ ifneq ($(HASNATDYNLINK),false)
PLUGINS:=$(PLUGINSCMA)
PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
else
+ifeq ($(BEST),byte)
+ STATICPLUGINS:=
+ INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
+ $(FUNINDCMA) $(NATSYNTAXCMA)
+ INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ PLUGINS:=$(PLUGINSCMA)
+ PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
+else
STATICPLUGINS:=$(PLUGINSCMA)
INITPLUGINS:=
INITPLUGINSOPT:=
PLUGINS:=
PLUGINSOPT:=
endif
+endif
LINKCMO:=$(CORECMA) $(STATICPLUGINS)
LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)