diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common index a1bfd0885..de84aaefe 100644 --- a/Makefile.common +++ b/Makefile.common @@ -204,6 +204,12 @@ else PLUGINSOPT:= endif +ifeq ($(BEST),opt) + INITPLUGINSBEST:=$(INITPLUGINSOPT) +else + INITPLUGINSBEST:=$(INITPLUGINS) +endif + CMA:=$(CLIBS) $(CAMLP4OBJS) CMXA:=$(CMA:.cma=.cmxa) |