aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-14 16:11:40 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-14 16:11:40 +0200
commit4782d1f9e7679f2a5cbf4fa487ecb4708e7683f6 (patch)
tree0dde487ef008f89ced86cad7fb4cb1d04c238e26 /Makefile.common
parenta1eeb3abe387a89cd5a9108160643b6157f9c0af (diff)
parent6c510a0d145d41e7250f121bfd01e0251e41af2c (diff)
Merge remote-tracking branch 'origin/pr/146' into trunk
Conflicts: Makefile.common
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common6
1 files changed, 4 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index 4742bb51e..95f4c01fd 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -61,7 +61,8 @@ PLUGINS:=\
omega romega micromega quote \
setoid_ring extraction fourier \
cc funind firstorder derive \
- rtauto nsatz syntax decl_mode btauto
+ rtauto nsatz syntax decl_mode btauto \
+ ssrmatching
SRCDIRS:=\
$(CORESRCDIRS) \
@@ -119,13 +120,14 @@ 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
PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
$(QUOTECMA) $(RINGCMA) \
$(FOURIERCMA) $(EXTRACTIONCMA) \
$(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
$(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \
- $(DERIVECMA)
+ $(DERIVECMA) $(SSRMATCHINGCMA)
ifneq ($(HASNATDYNLINK),false)
STATICPLUGINS:=