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.
---
 interp/constrextern.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c55e17e7a3..c198c4eb9b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -194,7 +194,6 @@ let without_specific_symbols l =
 let get_record_print =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"record printing"
     ~key:["Printing";"Records"]
     ~value:true
 
-- 
cgit v1.2.3