diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/Makefile.common b/Makefile.common index 71e85d7f06..5a981ae122 100644 --- a/Makefile.common +++ b/Makefile.common @@ -267,11 +267,6 @@ ifneq ($(HASNATDYNLINK),false) PLUGINS:=$(CONTRIBS) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINSOPT:=$(PLUGINS:.cma=.cmxs) - ifeq ($(BEST),opt) - INITPLUGINSBEST:=$(INITPLUGINSOPT) - else - INITPLUGINSBEST:=$(INITPLUGINS) - endif else CONTRIBSTATIC:=$(CONTRIBS) endif |