From 023d189aa201c8d5c71bc7de3e98725273d01b4f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 11 May 2020 17:41:58 +0200
Subject: Move SSR's Search to a new plugin and deprecate it.

---
 Makefile.common | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index d435d7dfad..8f880e93fb 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -106,7 +106,7 @@ PLUGINDIRS:=\
   setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
-  ssrmatching	ltac		ssr
+  ssrmatching	ltac		ssr             ssrsearch
 
 USERCONTRIBDIRS:=\
 	Ltac2
@@ -158,6 +158,7 @@ DERIVECMO:=plugins/derive/derive_plugin.cmo
 LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
+SSRSEARCHCMO=plugins/ssrsearch/ssrsearch_plugin.cmo
 LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
 ZIFYCMO:=plugins/micromega/zify_plugin.cmo
 
@@ -166,7 +167,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO) $(ZIFYCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(SSRSEARCHCMO) $(LTAC2CMO) $(ZIFYCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
-- 
cgit v1.2.3