From 19c8ac834c4f43b1fd0c49aad286a4e5bebf0ce5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 May 2020 16:47:30 +0200
Subject: Adding missing DECLARE PLUGIN so that compilation with -natdynlink no
 works.

---
 plugins/ssrsearch/g_search.mlg | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 6d68cc13ab..f5cbf2005b 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -2,6 +2,8 @@
 
 (* Main prefilter *)
 
+DECLARE PLUGIN "ssrsearch_plugin"
+
 {
 
 module CoqConstr = Constr
-- 
cgit v1.2.3