From 1b38f1256924df8897f1737e4b4124fbcc22c790 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 16 Jun 2016 14:27:20 +0200
Subject: Fix Makefile after ssrmatching merge

---
 Makefile.common | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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) \
-- 
cgit v1.2.3