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/firstorder/g_ground.mlg | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 9d208e1c86..930801f6fd 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -36,7 +36,6 @@ let ground_depth=ref 3
 let ()=
   let gdopt=
     { optdepr=false;
-      optname="Firstorder Depth";
       optkey=["Firstorder";"Depth"];
       optread=(fun ()->Some !ground_depth);
       optwrite=
-- 
cgit v1.2.3