From e047599a7851d5c757635e966067ca9271577692 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 21 Oct 2020 11:05:52 +0200
Subject: Remove warning on SSR Search having moved.

---
 plugins/ssrsearch/g_search.mlg | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'plugins/ssrsearch')

diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 5e002e09cc..54fdea0860 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -301,10 +301,6 @@ let ssrdisplaysearch gr env t =
   let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
   Feedback.msg_notice (hov 2 pr_res ++ fnl ())
 
-(* Remove the warning entirely when this plugin is loaded. *)
-let _ =
-  Ssreflect_plugin.Ssrvernac.warn_search_moved_enabled := false
-
 let deprecated_search =
   CWarnings.create
     ~name:"deprecated-ssr-search"
-- 
cgit v1.2.3