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.
---
 ide/protocol/interface.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'ide/protocol/interface.ml')

diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index 362833743e..be5e305ad3 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -71,8 +71,6 @@ type option_state = {
   (** Whether an option is synchronous *)
   opt_depr  : bool;
   (** Whether an option is deprecated *)
-  opt_name  : string;
-  (** A short string that is displayed when using [Test] *)
   opt_value : option_value;
   (** The current value of the option *)
 }
-- 
cgit v1.2.3