From 4563779bf990cf22d88474a68acf4eb9cfd8d173 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Feb 2020 17:07:34 +0100
Subject: Remove Goptions.opt_name field

The standard use is to repeat the option keywords in lowercase, which
is basically useless.

En passant add doc entry for Dump Arith.
---
 plugins/ssrmatching/ssrmatching.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 6cb464918a..2f6d69935a 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -55,8 +55,7 @@ let debug b =
   if b then pp_ref := ssr_pp else pp_ref := fun _ -> ()
 let _ =
   Goptions.declare_bool_option
-    { Goptions.optname  = "ssrmatching debugging";
-      Goptions.optkey   = ["Debug";"SsrMatching"];
+    { Goptions.optkey   = ["Debug";"SsrMatching"];
       Goptions.optdepr  = false;
       Goptions.optread  = (fun _ -> !pp_ref == ssr_pp);
       Goptions.optwrite = debug }
-- 
cgit v1.2.3