diff options
| author | Enrico Tassi | 2016-06-16 14:27:20 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-16 14:27:20 +0200 |
| commit | 1b38f1256924df8897f1737e4b4124fbcc22c790 (patch) | |
| tree | 7b48f1cc591f9ecc4f7d5dc65d899803caa2b60d /Makefile.common | |
| parent | 01847d2c992b05af5ed477ec7a208064526b0c5f (diff) | |
Fix Makefile after ssrmatching merge
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 95f4c01fd0..e156b101ca 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) \ |