diff options
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 95f4c01fd..e156b101c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -120,7 +120,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ string_syntax_plugin.cmo ) DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cmo DERIVECMA:=plugins/derive/derive_plugin.cmo -SSRMATCHINGCMA:=plugins/ssrmatching/ssrmatching.cmo +SSRMATCHINGCMA:=plugins/ssrmatching/ssrmatching_plugin.cmo PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) \ |