diff options
| -rw-r--r-- | Makefile.common | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index 3f8c2a0518..d18cf73d87 100644 --- a/Makefile.common +++ b/Makefile.common @@ -186,10 +186,9 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ string_syntax_plugin.cma ) DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma -PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \ +PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ - $(DECLMODECMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) |